1193
0 true
1 ( >= BC_width 0.0 )
2 ( >= BC_hight 0.0 )
3 ( <= BC_width 4000.0 )
4 ( <= BC_x 0.0 )
5 ( >= BC_x 0.0 )
6 ( <= BC_y 0.0 )
7 ( >= BC_y 0.0 )
8 BC_feasible
9 ( >= back_ground_width 0.0 )
10 ( >= back_ground_hight 0.0 )
11 ( >= title_x 0.0 )
12 ( >= title_width 0.0 )
13 ( >= main_holder_x 0.0 )
14 ( >= main_holder_width 0.0 )
15 ( >= main_holder_hight 0.0 )
16 ( >= title_y 0.0 )
17 ( >= back_ground_hight 80.0 )
18 ( >= main_holder_y 0.0 )
19 ( <= ( + main_holder_y main_holder_hight ( * -1.0 back_ground_hight ) ) 0.0 )
20 ( <= ( + title_x ( * -1.0 back_ground_x ) ) 0.0 )
21 ( >= ( + title_x ( * -1.0 back_ground_x ) ) 0.0 )
22 ( <= ( + main_holder_x ( * -1.0 back_ground_x ) ) 0.0 )
23 ( >= ( + main_holder_x ( * -1.0 back_ground_x ) ) 0.0 )
24 ( <= ( + title_x title_width ( * -1.0 back_ground_x ) ( * -1.0 back_ground_width ) ) 0.0 )
25 ( >= ( + title_x title_width ( * -1.0 back_ground_x ) ( * -1.0 back_ground_width ) ) 0.0 )
26 ( <= ( + main_holder_x main_holder_width ( * -1.0 back_ground_x ) ( * -1.0 back_ground_width ) ) 0.0 )
27 ( >= ( + main_holder_x main_holder_width ( * -1.0 back_ground_x ) ( * -1.0 back_ground_width ) ) 0.0 )
28 ( <= title_y 0.0 )
29 ( >= ( + main_holder_y main_holder_hight ( * -1.0 back_ground_hight ) ) 0.0 )
30 ( <= ( + main_holder_y ( * -1.0 title_y ) ( * -1.0 title_hight ) ) 0.0 )
31 ( >= ( + main_holder_y ( * -1.0 title_y ) ( * -1.0 title_hight ) ) 0.0 )
32 ( <= back_ground_x 0.0 )
33 ( >= back_ground_x 0.0 )
34 ( <= ( + BC_width ( * -1.0 back_ground_x ) ( * -1.0 back_ground_width ) ) 0.0 )
35 ( >= ( + BC_width ( * -1.0 back_ground_x ) ( * -1.0 back_ground_width ) ) 0.0 )
36 ( <= back_ground_y 0.0 )
37 ( >= back_ground_y 0.0 )
38 ( >= less_icon_x 0.0 )
39 ( >= less_icon_y 0.0 )
40 ( >= less_icon_hight 0.0 )
41 ( >= github_icon_x 0.0 )
42 ( >= github_icon_y 0.0 )
43 ( >= github_icon_hight 0.0 )
44 ( >= dashbord_x 0.0 )
45 ( >= dashbord_y 0.0 )
46 ( >= dashbord_hight 0.0 )
47 ( >= search_holder_x 0.0 )
48 ( >= search_holder_y 0.0 )
49 ( >= search_holder_width 0.0 )
50 ( >= search_holder_hight 0.0 )
51 ( >= mails_holder_x 0.0 )
52 ( >= mails_holder_y 0.0 )
53 ( >= mails_holder_width 0.0 )
54 ( >= mails_holder_hight 0.0 )
55 ( <= ( + less_icon_x ( * -1.0 title_x ) ( * -1.0 title_width ) ) -50.0 )
56 ( >= ( + github_icon_x ( * -1.0 title_x ) ) 0.0 )
57 ( <= ( + github_icon_x ( * -1.0 title_x ) ( * -1.0 title_width ) ) -50.0 )
58 ( >= ( + dashbord_x ( * -1.0 title_x ) ) 0.0 )
59 ( <= ( + dashbord_x ( * -1.0 title_x ) ( * -1.0 title_width ) ) -150.0 )
60 ( >= ( + search_holder_x ( * -1.0 title_x ) ) 0.0 )
61 ( <= ( + search_holder_width search_holder_x ( * -1.0 title_x ) ( * -1.0 title_width ) ) 0.0 )
62 ( >= ( + mails_holder_x ( * -1.0 title_x ) ) 0.0 )
63 ( >= ( + search_holder_x ( * -1.0 dashbord_width ) ( * -1.0 dashbord_x ) ) 0.0 )
64 ( <= title_hight 80.0 )
65 ( >= title_hight 80.0 )
66 ( <= ( + less_icon_x ( * -1.0 title_x ) ) 20.0 )
67 ( >= ( + less_icon_x ( * -1.0 title_x ) ) 20.0 )
68 ( <= ( + mails_holder_x mails_holder_width ( * -1.0 title_x ) ( * -1.0 title_width ) ) -20.0 )
69 ( >= ( + mails_holder_x mails_holder_width ( * -1.0 title_x ) ( * -1.0 title_width ) ) -20.0 )
70 ( <= ( + title_y ( * -1.0 less_icon_y ) ) -20.0 )
71 ( >= ( + title_y ( * -1.0 less_icon_y ) ) -20.0 )
72 ( <= ( + title_y ( * -1.0 github_icon_y ) ) -20.0 )
73 ( >= ( + title_y ( * -1.0 github_icon_y ) ) -20.0 )
74 ( <= ( + title_y ( * -1.0 dashbord_y ) ) -20.0 )
75 ( >= ( + title_y ( * -1.0 dashbord_y ) ) -20.0 )
76 ( <= ( + search_holder_y ( * -1.0 title_y ) ) 20.0 )
77 ( >= ( + search_holder_y ( * -1.0 title_y ) ) 20.0 )
78 ( <= ( + mails_holder_y ( * -1.0 title_y ) ) 20.0 )
79 ( >= ( + mails_holder_y ( * -1.0 title_y ) ) 20.0 )
80 ( <= ( + title_y title_hight ( * -1.0 less_icon_hight ) ( * -1.0 less_icon_y ) ) 20.0 )
81 ( >= ( + title_y title_hight ( * -1.0 less_icon_hight ) ( * -1.0 less_icon_y ) ) 20.0 )
82 ( <= ( + title_y title_hight ( * -1.0 github_icon_y ) ( * -1.0 github_icon_hight ) ) 20.0 )
83 ( >= ( + title_y title_hight ( * -1.0 github_icon_y ) ( * -1.0 github_icon_hight ) ) 20.0 )
84 ( <= ( + title_y title_hight ( * -1.0 dashbord_y ) ( * -1.0 dashbord_hight ) ) 20.0 )
85 ( >= ( + title_y title_hight ( * -1.0 dashbord_y ) ( * -1.0 dashbord_hight ) ) 20.0 )
86 ( <= ( + search_holder_y search_holder_hight ( * -1.0 title_y ) ( * -1.0 title_hight ) ) -20.0 )
87 ( >= ( + search_holder_y search_holder_hight ( * -1.0 title_y ) ( * -1.0 title_hight ) ) -20.0 )
88 ( <= ( + mails_holder_y mails_holder_hight ( * -1.0 title_y ) ( * -1.0 title_hight ) ) -20.0 )
89 ( >= ( + mails_holder_y mails_holder_hight ( * -1.0 title_y ) ( * -1.0 title_hight ) ) -20.0 )
90 ( <= less_icon_width 50.0 )
91 ( >= less_icon_width 50.0 )
92 ( <= ( + github_icon_x ( * -1.0 less_icon_x ) ( * -1.0 less_icon_width ) ) 10.0 )
93 ( >= ( + github_icon_x ( * -1.0 less_icon_x ) ( * -1.0 less_icon_width ) ) 10.0 )
94 ( <= github_icon_width 50.0 )
95 ( >= github_icon_width 50.0 )
96 ( <= ( + dashbord_x ( * -1.0 github_icon_x ) ( * -1.0 github_icon_width ) ) 10.0 )
97 ( >= ( + dashbord_x ( * -1.0 github_icon_x ) ( * -1.0 github_icon_width ) ) 10.0 )
98 ( <= dashbord_width 150.0 )
99 ( >= dashbord_width 150.0 )
100 ( >= search_bar_1_x 0.0 )
101 ( >= search_bar_1_y 0.0 )
102 ( >= search_bar_1_hight 0.0 )
103 ( >= search_bar_2_x 0.0 )
104 ( >= search_bar_2_y 0.0 )
105 ( >= search_bar_2_hight 0.0 )
106 search_bar_1_feasible
107 ( <= ( + search_holder_x ( * -1.0 search_bar_1_x ) ) 0.0 )
108 ( >= ( + search_holder_x ( * -1.0 search_bar_1_x ) ) 0.0 )
109 ( <= ( + search_holder_width search_holder_x ( * -1.0 search_bar_1_x ) ( * -1.0 search_bar_1_width ) ) 0.0 )
110 ( >= ( + search_holder_width search_holder_x ( * -1.0 search_bar_1_x ) ( * -1.0 search_bar_1_width ) ) 0.0 )
111 ( <= ( + search_bar_1_y ( * -1.0 search_holder_y ) ) 0.0 )
112 ( >= ( + search_bar_1_y ( * -1.0 search_holder_y ) ) 0.0 )
113 ( <= ( + search_bar_1_y search_bar_1_hight ( * -1.0 search_holder_y ) ( * -1.0 search_holder_hight ) ) 0.0 )
114 ( >= ( + search_bar_1_y search_bar_1_hight ( * -1.0 search_holder_y ) ( * -1.0 search_holder_hight ) ) 0.0 )
115 search_bar_2_feasible
116 ( <= ( + search_holder_x ( * -1.0 search_bar_2_x ) ) 0.0 )
117 ( >= ( + search_holder_x ( * -1.0 search_bar_2_x ) ) 0.0 )
118 ( <= ( + search_holder_width search_holder_x ( * -1.0 search_bar_2_x ) ) 50.0 )
119 ( >= ( + search_holder_width search_holder_x ( * -1.0 search_bar_2_x ) ) 50.0 )
120 ( <= ( + search_holder_y ( * -1.0 search_bar_2_y ) ) 0.0 )
121 ( >= ( + search_holder_y ( * -1.0 search_bar_2_y ) ) 0.0 )
122 ( <= ( + search_bar_2_hight ( * -1.0 search_holder_y ) ( * -1.0 search_holder_hight ) search_bar_2_y ) 0.0 )
123 ( >= ( + search_bar_2_hight ( * -1.0 search_holder_y ) ( * -1.0 search_holder_hight ) search_bar_2_y ) 0.0 )
124 ( <= search_bar_1_width 300.0 )
125 ( >= search_bar_1_width 300.0 )
126 ( <= search_bar_2_width 50.0 )
127 ( >= search_bar_2_width 50.0 )
128 ( >= ( + search_holder_x ( * -1.0 dashbord_width ) ( * -1.0 dashbord_x ) ) 200.0 )
129 ( >= search_bar_1_kid_0_x 0.0 )
130 ( >= search_bar_1_kid_0_y 0.0 )
131 ( >= search_bar_1_kid_0_width 0.0 )
132 ( >= search_bar_1_kid_0_hight 0.0 )
133 ( >= search_bar_1_kid_1_x 0.0 )
134 ( >= search_bar_1_kid_1_y 0.0 )
135 ( >= search_bar_1_kid_1_width 0.0 )
136 ( >= search_bar_1_kid_1_hight 0.0 )
137 ( <= ( + search_bar_1_kid_0_width ( * -1.0 search_bar_1_kid_1_x ) search_bar_1_kid_0_x ) 0.0 )
138 ( >= ( + search_bar_1_kid_0_width ( * -1.0 search_bar_1_kid_1_x ) search_bar_1_kid_0_x ) 0.0 )
139 ( <= ( + search_bar_1_x ( * -1.0 search_bar_1_kid_0_x ) ) 0.0 )
140 ( >= ( + search_bar_1_x ( * -1.0 search_bar_1_kid_0_x ) ) 0.0 )
141 ( <= ( + search_bar_1_kid_1_width ( * -1.0 search_bar_1_x ) ( * -1.0 search_bar_1_width ) search_bar_1_kid_1_x ) 0.0 )
142 ( >= ( + search_bar_1_kid_1_width ( * -1.0 search_bar_1_x ) ( * -1.0 search_bar_1_width ) search_bar_1_kid_1_x ) 0.0 )
143 ( <= ( + search_bar_1_y ( * -1.0 search_bar_1_kid_0_y ) ) 0.0 )
144 ( >= ( + search_bar_1_y ( * -1.0 search_bar_1_kid_0_y ) ) 0.0 )
145 ( <= ( + search_bar_1_y ( * -1.0 search_bar_1_kid_1_y ) ) 0.0 )
146 ( >= ( + search_bar_1_y ( * -1.0 search_bar_1_kid_1_y ) ) 0.0 )
147 ( <= ( + search_bar_1_y search_bar_1_hight ( * -1.0 search_bar_1_kid_0_hight ) ( * -1.0 search_bar_1_kid_0_y ) ) 0.0 )
148 ( >= ( + search_bar_1_y search_bar_1_hight ( * -1.0 search_bar_1_kid_0_hight ) ( * -1.0 search_bar_1_kid_0_y ) ) 0.0 )
149 ( <= ( + search_bar_1_y search_bar_1_hight ( * -1.0 search_bar_1_kid_1_y ) ( * -1.0 search_bar_1_kid_1_hight ) ) 0.0 )
150 ( >= ( + search_bar_1_y search_bar_1_hight ( * -1.0 search_bar_1_kid_1_y ) ( * -1.0 search_bar_1_kid_1_hight ) ) 0.0 )
151 ( <= search_bar_1_kid_0_width 40.0 )
152 ( >= search_bar_1_kid_0_width 40.0 )
153 ( >= mails_1_x 0.0 )
154 ( >= mails_1_y 0.0 )
155 ( >= mails_1_width 0.0 )
156 ( >= mails_1_hight 0.0 )
157 ( >= mails_2_x 0.0 )
158 ( >= mails_2_y 0.0 )
159 ( >= mails_2_width 0.0 )
160 ( >= mails_2_hight 0.0 )
161 mails_1_feasible
162 ( <= ( + mails_1_x ( * -1.0 mails_holder_x ) ) 0.0 )
163 ( >= ( + mails_1_x ( * -1.0 mails_holder_x ) ) 0.0 )
164 ( <= ( + mails_1_x mails_1_width ( * -1.0 mails_holder_x ) ( * -1.0 mails_holder_width ) ) 0.0 )
165 ( >= ( + mails_1_x mails_1_width ( * -1.0 mails_holder_x ) ( * -1.0 mails_holder_width ) ) 0.0 )
166 ( <= ( + mails_1_y ( * -1.0 mails_holder_y ) ) 0.0 )
167 ( >= ( + mails_1_y ( * -1.0 mails_holder_y ) ) 0.0 )
168 ( <= ( + mails_1_y mails_1_hight ( * -1.0 mails_holder_y ) ( * -1.0 mails_holder_hight ) ) 0.0 )
169 ( >= ( + mails_1_y mails_1_hight ( * -1.0 mails_holder_y ) ( * -1.0 mails_holder_hight ) ) 0.0 )
170 mails_2_feasible
171 ( <= ( + mails_2_x ( * -1.0 mails_holder_x ) ) 0.0 )
172 ( >= ( + mails_2_x ( * -1.0 mails_holder_x ) ) 0.0 )
173 ( <= ( + mails_2_width mails_2_x ( * -1.0 mails_holder_x ) ( * -1.0 mails_holder_width ) ) 0.0 )
174 ( >= ( + mails_2_width mails_2_x ( * -1.0 mails_holder_x ) ( * -1.0 mails_holder_width ) ) 0.0 )
175 ( <= ( + mails_2_y ( * -1.0 mails_holder_y ) ) 0.0 )
176 ( >= ( + mails_2_y ( * -1.0 mails_holder_y ) ) 0.0 )
177 ( <= ( + mails_2_y mails_2_hight ( * -1.0 mails_holder_y ) ( * -1.0 mails_holder_hight ) ) 0.0 )
178 ( >= ( + mails_2_y mails_2_hight ( * -1.0 mails_holder_y ) ( * -1.0 mails_holder_hight ) ) 0.0 )
179 ( <= ( + search_holder_width ( * -1.0 mails_holder_x ) search_holder_x ) -10.0 )
180 ( >= ( + search_holder_width ( * -1.0 mails_holder_x ) search_holder_x ) -10.0 )
181 ( >= add_x 0.0 )
182 ( >= add_y 0.0 )
183 ( >= add_hight 0.0 )
184 ( >= point_x 0.0 )
185 ( >= point_y 0.0 )
186 ( >= point_hight 0.0 )
187 ( >= pull_x 0.0 )
188 ( >= pull_y 0.0 )
189 ( >= pull_hight 0.0 )
190 ( >= mail_x 0.0 )
191 ( >= mail_y 0.0 )
192 ( >= mail_hight 0.0 )
193 ( >= person_x 0.0 )
194 ( >= person_y 0.0 )
195 ( >= person_hight 0.0 )
196 ( >= ( + add_x ( * -1.0 mails_1_x ) ) 0.0 )
197 ( <= ( + add_x ( * -1.0 mails_1_x ) ( * -1.0 mails_1_width ) ) -100.0 )
198 ( <= ( + mails_1_y ( * -1.0 add_y ) ) 0.0 )
199 ( >= ( + mails_1_y mails_1_hight ( * -1.0 add_y ) ( * -1.0 add_hight ) ) 0.0 )
200 ( >= ( + point_x ( * -1.0 mails_1_x ) ) 0.0 )
201 ( <= ( + point_x ( * -1.0 mails_1_x ) ( * -1.0 mails_1_width ) ) -50.0 )
202 ( <= ( + mails_1_y ( * -1.0 point_y ) ) 0.0 )
203 ( >= ( + mails_1_y mails_1_hight ( * -1.0 point_y ) ( * -1.0 point_hight ) ) 0.0 )
204 ( >= ( + pull_x ( * -1.0 mails_1_x ) ) 0.0 )
205 ( <= ( + pull_x ( * -1.0 mails_1_x ) ( * -1.0 mails_1_width ) ) -50.0 )
206 ( <= ( + mails_1_y ( * -1.0 pull_y ) ) 0.0 )
207 ( >= ( + mails_1_y mails_1_hight ( * -1.0 pull_hight ) ( * -1.0 pull_y ) ) 0.0 )
208 ( >= ( + mail_x ( * -1.0 mails_1_x ) ) 0.0 )
209 ( <= ( + mail_x ( * -1.0 mails_1_x ) ( * -1.0 mails_1_width ) ) -50.0 )
210 ( >= ( + mail_y ( * -1.0 mails_1_y ) ) 0.0 )
211 ( <= ( + mail_hight mail_y ( * -1.0 mails_1_y ) ( * -1.0 mails_1_hight ) ) 0.0 )
212 ( >= ( + person_x ( * -1.0 mails_1_x ) ) 0.0 )
213 ( <= ( + person_x ( * -1.0 mails_1_x ) ( * -1.0 mails_1_width ) ) -50.0 )
214 ( >= ( + person_y ( * -1.0 mails_1_y ) ) 0.0 )
215 ( <= ( + person_y person_hight ( * -1.0 mails_1_y ) ( * -1.0 mails_1_hight ) ) 0.0 )
216 ( >= ( + point_x ( * -1.0 add_x ) ) 100.0 )
217 ( >= ( + pull_x ( * -1.0 point_x ) ) 50.0 )
218 ( >= ( + mail_x ( * -1.0 pull_x ) ) 50.0 )
219 ( <= ( + mail_x mail_width ( * -1.0 person_x ) ) 0.0 )
220 ( <= ( + add_x ( * -1.0 mails_1_x ) ) 0.0 )
221 ( >= ( + person_x ( * -1.0 mails_1_x ) ( * -1.0 mails_1_width ) ) -50.0 )
222 ( >= ( + mails_1_y ( * -1.0 add_y ) ) 0.0 )
223 ( >= ( + mails_1_y ( * -1.0 point_y ) ) 0.0 )
224 ( >= ( + mails_1_y ( * -1.0 pull_y ) ) 0.0 )
225 ( <= ( + mail_y ( * -1.0 mails_1_y ) ) 0.0 )
226 ( <= ( + person_y ( * -1.0 mails_1_y ) ) 0.0 )
227 ( <= ( + mails_1_y mails_1_hight ( * -1.0 add_y ) ( * -1.0 add_hight ) ) 0.0 )
228 ( <= ( + mails_1_y mails_1_hight ( * -1.0 point_y ) ( * -1.0 point_hight ) ) 0.0 )
229 ( <= ( + mails_1_y mails_1_hight ( * -1.0 pull_hight ) ( * -1.0 pull_y ) ) 0.0 )
230 ( >= ( + mail_hight mail_y ( * -1.0 mails_1_y ) ( * -1.0 mails_1_hight ) ) 0.0 )
231 ( >= ( + person_y person_hight ( * -1.0 mails_1_y ) ( * -1.0 mails_1_hight ) ) 0.0 )
232 ( <= ( + point_x ( * -1.0 add_x ) ) 110.0 )
233 ( >= ( + point_x ( * -1.0 add_x ) ) 110.0 )
234 ( <= ( + pull_x ( * -1.0 point_x ) ) 60.0 )
235 ( >= ( + pull_x ( * -1.0 point_x ) ) 60.0 )
236 ( <= ( + mail_x ( * -1.0 pull_x ) ) 60.0 )
237 ( >= ( + mail_x ( * -1.0 pull_x ) ) 60.0 )
238 ( <= ( + mail_x mail_width ( * -1.0 person_x ) ) -10.0 )
239 ( >= ( + mail_x mail_width ( * -1.0 person_x ) ) -10.0 )
240 ( <= add_width 100.0 )
241 ( >= add_width 100.0 )
242 ( <= point_width 50.0 )
243 ( >= point_width 50.0 )
244 ( <= pull_width 50.0 )
245 ( >= pull_width 50.0 )
246 ( <= mail_width 50.0 )
247 ( >= mail_width 50.0 )
248 ( <= person_width 50.0 )
249 ( >= person_width 50.0 )
250 ( <= ( + mail_x ( * -1.0 mails_2_x ) ) 0.0 )
251 ( >= ( + mail_x ( * -1.0 mails_2_x ) ) 0.0 )
252 ( <= ( + person_x ( * -1.0 mails_2_width ) ( * -1.0 mails_2_x ) ) -50.0 )
253 ( >= ( + person_x ( * -1.0 mails_2_width ) ( * -1.0 mails_2_x ) ) -50.0 )
254 ( <= ( + mails_2_y ( * -1.0 mail_y ) ) 0.0 )
255 ( >= ( + mails_2_y ( * -1.0 mail_y ) ) 0.0 )
256 ( <= ( + mails_2_y ( * -1.0 person_y ) ) 0.0 )
257 ( >= ( + mails_2_y ( * -1.0 person_y ) ) 0.0 )
258 ( <= ( + mails_2_y mails_2_hight ( * -1.0 mail_hight ) ( * -1.0 mail_y ) ) 0.0 )
259 ( >= ( + mails_2_y mails_2_hight ( * -1.0 mail_hight ) ( * -1.0 mail_y ) ) 0.0 )
260 ( <= ( + mails_2_y ( * -1.0 person_y ) mails_2_hight ( * -1.0 person_hight ) ) 0.0 )
261 ( >= ( + mails_2_y ( * -1.0 person_y ) mails_2_hight ( * -1.0 person_hight ) ) 0.0 )
262 ( <= ( + mail_x ( * -1.0 mails_2_width ) ( * -1.0 mails_2_x ) ) -50.0 )
263 ( >= ( + person_x ( * -1.0 mails_2_x ) ) 0.0 )
264 ( >= main_2_collom_x 0.0 )
265 ( >= main_2_collom_y 0.0 )
266 ( >= main_2_collom_width 0.0 )
267 ( >= main_2_collom_hight 0.0 )
268 ( >= main_1_collom_x 0.0 )
269 ( >= main_1_collom_y 0.0 )
270 ( >= main_1_collom_width 0.0 )
271 ( >= main_1_collom_hight 0.0 )
272 main_2_collom_feasible
273 ( <= ( + main_2_collom_x ( * -1.0 main_holder_x ) ) 0.0 )
274 ( >= ( + main_2_collom_x ( * -1.0 main_holder_x ) ) 0.0 )
275 ( <= ( + main_2_collom_width main_2_collom_x ( * -1.0 main_holder_x ) ( * -1.0 main_holder_width ) ) 0.0 )
276 ( >= ( + main_2_collom_width main_2_collom_x ( * -1.0 main_holder_x ) ( * -1.0 main_holder_width ) ) 0.0 )
277 ( <= ( + main_2_collom_y ( * -1.0 main_holder_y ) ) 0.0 )
278 ( >= ( + main_2_collom_y ( * -1.0 main_holder_y ) ) 0.0 )
279 ( <= ( + main_2_collom_y main_2_collom_hight ( * -1.0 main_holder_y ) ( * -1.0 main_holder_hight ) ) 0.0 )
280 ( >= ( + main_2_collom_y main_2_collom_hight ( * -1.0 main_holder_y ) ( * -1.0 main_holder_hight ) ) 0.0 )
281 main_1_collom_feasible
282 ( <= ( + main_1_collom_x ( * -1.0 main_holder_x ) ) 0.0 )
283 ( >= ( + main_1_collom_x ( * -1.0 main_holder_x ) ) 0.0 )
284 ( <= ( + main_1_collom_width main_1_collom_x ( * -1.0 main_holder_x ) ( * -1.0 main_holder_width ) ) 0.0 )
285 ( >= ( + main_1_collom_width main_1_collom_x ( * -1.0 main_holder_x ) ( * -1.0 main_holder_width ) ) 0.0 )
286 ( <= ( + main_1_collom_y ( * -1.0 main_holder_y ) ) 0.0 )
287 ( >= ( + main_1_collom_y ( * -1.0 main_holder_y ) ) 0.0 )
288 ( <= ( + main_1_collom_y main_1_collom_hight ( * -1.0 main_holder_y ) ( * -1.0 main_holder_hight ) ) 0.0 )
289 ( >= ( + main_1_collom_y main_1_collom_hight ( * -1.0 main_holder_y ) ( * -1.0 main_holder_hight ) ) 0.0 )
290 ( >= side_bar_x 0.0 )
291 ( >= side_bar_y 0.0 )
292 ( >= side_bar_width 0.0 )
293 ( >= side_bar_hight 0.0 )
294 ( >= home_collom_x 0.0 )
295 ( >= home_collom_y 0.0 )
296 ( >= home_collom_width 0.0 )
297 ( >= home_collom_hight 0.0 )
298 ( >= ( + side_bar_x ( * -1.0 main_2_collom_x ) ) 0.0 )
299 ( <= ( + side_bar_x side_bar_width ( * -1.0 main_2_collom_width ) ( * -1.0 main_2_collom_x ) ) 0.0 )
300 ( >= ( + side_bar_y ( * -1.0 main_2_collom_y ) ) 0.0 )
301 ( <= ( + side_bar_y side_bar_hight ( * -1.0 main_2_collom_y ) ( * -1.0 main_2_collom_hight ) ) 0.0 )
302 ( >= ( + home_collom_x ( * -1.0 main_2_collom_x ) ) 0.0 )
303 ( <= ( + home_collom_width home_collom_x ( * -1.0 main_2_collom_width ) ( * -1.0 main_2_collom_x ) ) 0.0 )
304 ( >= ( + home_collom_y ( * -1.0 main_2_collom_y ) ) 0.0 )
305 ( <= ( + home_collom_y home_collom_hight ( * -1.0 main_2_collom_y ) ( * -1.0 main_2_collom_hight ) ) 0.0 )
306 ( <= ( + side_bar_x side_bar_width ( * -1.0 home_collom_x ) ) 0.0 )
307 ( <= ( + side_bar_x ( * -1.0 main_2_collom_x ) ) 0.0 )
308 ( >= ( + home_collom_width home_collom_x ( * -1.0 main_2_collom_width ) ( * -1.0 main_2_collom_x ) ) 0.0 )
309 ( <= ( + side_bar_y ( * -1.0 main_2_collom_y ) ) 0.0 )
310 ( <= ( + home_collom_y ( * -1.0 main_2_collom_y ) ) 0.0 )
311 ( >= ( + side_bar_y side_bar_hight ( * -1.0 main_2_collom_y ) ( * -1.0 main_2_collom_hight ) ) 0.0 )
312 ( >= ( + home_collom_y home_collom_hight ( * -1.0 main_2_collom_y ) ( * -1.0 main_2_collom_hight ) ) 0.0 )
313 ( >= ( + side_bar_x side_bar_width ( * -1.0 home_collom_x ) ) 0.0 )
314 ( >= user_name_x 0.0 )
315 ( >= user_name_y 0.0 )
316 ( >= user_name_width 0.0 )
317 ( >= top_repo_x 0.0 )
318 ( >= top_repo_y 0.0 )
319 ( >= top_repo_width 0.0 )
320 ( >= find_repo_x 0.0 )
321 ( >= find_repo_y 0.0 )
322 ( >= find_repo_width 0.0 )
323 ( >= repos_x 0.0 )
324 ( >= repos_y 0.0 )
325 ( >= repos_width 0.0 )
326 ( >= show_more_x 0.0 )
327 ( >= show_more_y 0.0 )
328 ( >= show_more_width 0.0 )
329 side_bar_feasible
330 ( <= ( + user_name_y ( * -1.0 top_repo_y ) ) -70.0 )
331 ( >= ( + user_name_y ( * -1.0 top_repo_y ) ) -70.0 )
332 ( <= ( + find_repo_y ( * -1.0 top_repo_y ) ) 70.0 )
333 ( >= ( + find_repo_y ( * -1.0 top_repo_y ) ) 70.0 )
334 ( <= ( + repos_y ( * -1.0 find_repo_y ) ) 70.0 )
335 ( >= ( + repos_y ( * -1.0 find_repo_y ) ) 70.0 )
336 ( <= ( + repos_y ( * -1.0 show_more_y ) ) -320.0 )
337 ( >= ( + repos_y ( * -1.0 show_more_y ) ) -320.0 )
338 ( <= ( + side_bar_x ( * -1.0 user_name_x ) ) -20.0 )
339 ( >= ( + side_bar_x side_bar_width ( * -1.0 user_name_width ) ( * -1.0 user_name_x ) ) 20.0 )
340 ( <= ( + side_bar_y ( * -1.0 user_name_y ) ) -20.0 )
341 ( >= ( + side_bar_y side_bar_hight ( * -1.0 user_name_y ) ) 70.0 )
342 ( <= ( + side_bar_x ( * -1.0 top_repo_x ) ) -20.0 )
343 ( >= ( + side_bar_x side_bar_width ( * -1.0 top_repo_x ) ( * -1.0 top_repo_width ) ) 20.0 )
344 ( <= ( + side_bar_y ( * -1.0 top_repo_y ) ) -20.0 )
345 ( >= ( + side_bar_y side_bar_hight ( * -1.0 top_repo_y ) ) 70.0 )
346 ( <= ( + side_bar_x ( * -1.0 find_repo_x ) ) -20.0 )
347 ( >= ( + side_bar_x side_bar_width ( * -1.0 find_repo_width ) ( * -1.0 find_repo_x ) ) 20.0 )
348 ( <= ( + side_bar_y ( * -1.0 find_repo_y ) ) -20.0 )
349 ( >= ( + side_bar_y side_bar_hight ( * -1.0 find_repo_y ) ) 70.0 )
350 ( <= ( + side_bar_x ( * -1.0 repos_x ) ) -20.0 )
351 ( >= ( + side_bar_x side_bar_width ( * -1.0 repos_x ) ( * -1.0 repos_width ) ) 20.0 )
352 ( <= ( + side_bar_y ( * -1.0 repos_y ) ) -20.0 )
353 ( >= ( + side_bar_y side_bar_hight ( * -1.0 repos_y ) ( * -1.0 repos_hight ) ) 20.0 )
354 ( <= ( + side_bar_x ( * -1.0 show_more_x ) ) -20.0 )
355 ( >= ( + side_bar_x side_bar_width ( * -1.0 show_more_width ) ( * -1.0 show_more_x ) ) 20.0 )
356 ( <= ( + side_bar_y ( * -1.0 show_more_y ) ) -20.0 )
357 ( >= ( + side_bar_y side_bar_hight ( * -1.0 show_more_y ) ) 70.0 )
358 ( <= ( + user_name_y ( * -1.0 top_repo_y ) ) -50.0 )
359 ( >= ( + find_repo_y ( * -1.0 top_repo_y ) ) 50.0 )
360 ( >= ( + repos_y ( * -1.0 find_repo_y ) ) 50.0 )
361 ( <= ( + repos_y ( * -1.0 show_more_y ) ) -300.0 )
362 ( <= side_bar_width 300.0 )
363 ( >= side_bar_width 300.0 )
364 ( >= ( + side_bar_x ( * -1.0 user_name_x ) ) -20.0 )
365 ( >= ( + side_bar_x ( * -1.0 top_repo_x ) ) -20.0 )
366 ( >= ( + side_bar_x ( * -1.0 find_repo_x ) ) -20.0 )
367 ( >= ( + side_bar_x ( * -1.0 repos_x ) ) -20.0 )
368 ( >= ( + side_bar_x ( * -1.0 show_more_x ) ) -20.0 )
369 ( <= user_name_hight 50.0 )
370 ( >= user_name_hight 50.0 )
371 ( <= user_name_width 100.0 )
372 ( >= user_name_width 100.0 )
373 ( >= ( + side_bar_y ( * -1.0 user_name_y ) ) -20.0 )
374 ( <= top_repo_hight 50.0 )
375 ( >= top_repo_hight 50.0 )
376 ( <= ( + side_bar_x side_bar_width ( * -1.0 top_repo_x ) ( * -1.0 top_repo_width ) ) 20.0 )
377 ( <= find_repo_hight 50.0 )
378 ( >= find_repo_hight 50.0 )
379 ( <= ( + side_bar_x side_bar_width ( * -1.0 find_repo_width ) ( * -1.0 find_repo_x ) ) 20.0 )
380 ( <= repos_hight 300.0 )
381 ( >= repos_hight 300.0 )
382 ( <= ( + side_bar_x side_bar_width ( * -1.0 repos_x ) ( * -1.0 repos_width ) ) 20.0 )
383 ( >= repos_kid_0_x 0.0 )
384 ( >= repos_kid_0_y 0.0 )
385 ( >= repos_kid_0_width 0.0 )
386 ( >= repos_kid_0_hight 0.0 )
387 ( >= repos_kid_1_x 0.0 )
388 ( >= repos_kid_1_y 0.0 )
389 ( >= repos_kid_1_width 0.0 )
390 ( >= repos_kid_1_hight 0.0 )
391 ( >= repos_kid_2_x 0.0 )
392 ( >= repos_kid_2_y 0.0 )
393 ( >= repos_kid_2_width 0.0 )
394 ( >= repos_kid_2_hight 0.0 )
395 ( >= repos_kid_3_x 0.0 )
396 ( >= repos_kid_3_y 0.0 )
397 ( >= repos_kid_3_width 0.0 )
398 ( >= repos_kid_3_hight 0.0 )
399 ( >= repos_kid_4_x 0.0 )
400 ( >= repos_kid_4_y 0.0 )
401 ( >= repos_kid_4_width 0.0 )
402 ( >= repos_kid_4_hight 0.0 )
403 ( >= repos_kid_5_x 0.0 )
404 ( >= repos_kid_5_y 0.0 )
405 ( >= repos_kid_5_width 0.0 )
406 ( >= repos_kid_5_hight 0.0 )
407 ( >= repos_kid_6_x 0.0 )
408 ( >= repos_kid_6_y 0.0 )
409 ( >= repos_kid_6_width 0.0 )
410 ( >= repos_kid_6_hight 0.0 )
411 repos_feasible
412 ( <= ( + repos_x ( * -1.0 repos_kid_0_x ) ) 0.0 )
413 ( >= ( + repos_x ( * -1.0 repos_kid_0_x ) ) 0.0 )
414 ( <= ( + repos_x ( * -1.0 repos_kid_1_x ) ) 0.0 )
415 ( >= ( + repos_x ( * -1.0 repos_kid_1_x ) ) 0.0 )
416 ( <= ( + repos_x ( * -1.0 repos_kid_2_x ) ) 0.0 )
417 ( >= ( + repos_x ( * -1.0 repos_kid_2_x ) ) 0.0 )
418 ( <= ( + repos_x ( * -1.0 repos_kid_3_x ) ) 0.0 )
419 ( >= ( + repos_x ( * -1.0 repos_kid_3_x ) ) 0.0 )
420 ( <= ( + repos_x ( * -1.0 repos_kid_4_x ) ) 0.0 )
421 ( >= ( + repos_x ( * -1.0 repos_kid_4_x ) ) 0.0 )
422 ( <= ( + repos_x ( * -1.0 repos_kid_5_x ) ) 0.0 )
423 ( >= ( + repos_x ( * -1.0 repos_kid_5_x ) ) 0.0 )
424 ( <= ( + repos_kid_6_x ( * -1.0 repos_x ) ) 0.0 )
425 ( >= ( + repos_kid_6_x ( * -1.0 repos_x ) ) 0.0 )
426 ( <= ( + repos_x repos_width ( * -1.0 repos_kid_0_x ) ( * -1.0 repos_kid_0_width ) ) 0.0 )
427 ( >= ( + repos_x repos_width ( * -1.0 repos_kid_0_x ) ( * -1.0 repos_kid_0_width ) ) 0.0 )
428 ( <= ( + repos_x repos_width ( * -1.0 repos_kid_1_x ) ( * -1.0 repos_kid_1_width ) ) 0.0 )
429 ( >= ( + repos_x repos_width ( * -1.0 repos_kid_1_x ) ( * -1.0 repos_kid_1_width ) ) 0.0 )
430 ( <= ( + repos_x repos_width ( * -1.0 repos_kid_2_x ) ( * -1.0 repos_kid_2_width ) ) 0.0 )
431 ( >= ( + repos_x repos_width ( * -1.0 repos_kid_2_x ) ( * -1.0 repos_kid_2_width ) ) 0.0 )
432 ( <= ( + repos_x repos_width ( * -1.0 repos_kid_3_x ) ( * -1.0 repos_kid_3_width ) ) 0.0 )
433 ( >= ( + repos_x repos_width ( * -1.0 repos_kid_3_x ) ( * -1.0 repos_kid_3_width ) ) 0.0 )
434 ( <= ( + repos_x repos_width ( * -1.0 repos_kid_4_width ) ( * -1.0 repos_kid_4_x ) ) 0.0 )
435 ( >= ( + repos_x repos_width ( * -1.0 repos_kid_4_width ) ( * -1.0 repos_kid_4_x ) ) 0.0 )
436 ( <= ( + repos_x repos_width ( * -1.0 repos_kid_5_x ) ( * -1.0 repos_kid_5_width ) ) 0.0 )
437 ( >= ( + repos_x repos_width ( * -1.0 repos_kid_5_x ) ( * -1.0 repos_kid_5_width ) ) 0.0 )
438 ( <= ( + repos_kid_6_x ( * -1.0 repos_x ) ( * -1.0 repos_width ) repos_kid_6_width ) 0.0 )
439 ( >= ( + repos_kid_6_x ( * -1.0 repos_x ) ( * -1.0 repos_width ) repos_kid_6_width ) 0.0 )
440 ( <= ( + repos_kid_0_y ( * -1.0 repos_y ) ) 0.0 )
441 ( >= ( + repos_kid_0_y ( * -1.0 repos_y ) ) 0.0 )
442 ( <= ( + repos_kid_6_hight repos_kid_6_y ( * -1.0 repos_y ) ( * -1.0 repos_hight ) ) 0.0 )
443 ( >= ( + repos_kid_6_hight repos_kid_6_y ( * -1.0 repos_y ) ( * -1.0 repos_hight ) ) 0.0 )
444 ( <= ( + repos_kid_0_hight ( * -1.0 repos_kid_1_y ) repos_kid_0_y ) -10.0 )
445 ( >= ( + repos_kid_0_hight ( * -1.0 repos_kid_1_y ) repos_kid_0_y ) -10.0 )
446 ( <= ( + repos_kid_1_hight ( * -1.0 repos_kid_2_y ) repos_kid_1_y ) -10.0 )
447 ( >= ( + repos_kid_1_hight ( * -1.0 repos_kid_2_y ) repos_kid_1_y ) -10.0 )
448 ( <= ( + repos_kid_2_hight ( * -1.0 repos_kid_3_y ) repos_kid_2_y ) -10.0 )
449 ( >= ( + repos_kid_2_hight ( * -1.0 repos_kid_3_y ) repos_kid_2_y ) -10.0 )
450 ( <= ( + repos_kid_3_hight ( * -1.0 repos_kid_4_y ) repos_kid_3_y ) -10.0 )
451 ( >= ( + repos_kid_3_hight ( * -1.0 repos_kid_4_y ) repos_kid_3_y ) -10.0 )
452 ( <= ( + repos_kid_4_hight ( * -1.0 repos_kid_5_y ) repos_kid_4_y ) -10.0 )
453 ( >= ( + repos_kid_4_hight ( * -1.0 repos_kid_5_y ) repos_kid_4_y ) -10.0 )
454 ( <= ( + repos_kid_5_hight repos_kid_5_y ( * -1.0 repos_kid_6_y ) ) -10.0 )
455 ( >= ( + repos_kid_5_hight repos_kid_5_y ( * -1.0 repos_kid_6_y ) ) -10.0 )
456 ( <= ( + repos_kid_0_hight ( * -1.0 repos_kid_1_hight ) ) 0.0 )
457 ( >= ( + repos_kid_0_hight ( * -1.0 repos_kid_1_hight ) ) 0.0 )
458 ( <= ( + repos_kid_0_hight ( * -1.0 repos_kid_2_hight ) ) 0.0 )
459 ( >= ( + repos_kid_0_hight ( * -1.0 repos_kid_2_hight ) ) 0.0 )
460 ( <= ( + repos_kid_0_hight ( * -1.0 repos_kid_3_hight ) ) 0.0 )
461 ( >= ( + repos_kid_0_hight ( * -1.0 repos_kid_3_hight ) ) 0.0 )
462 ( <= ( + repos_kid_0_hight ( * -1.0 repos_kid_4_hight ) ) 0.0 )
463 ( >= ( + repos_kid_0_hight ( * -1.0 repos_kid_4_hight ) ) 0.0 )
464 ( <= ( + repos_kid_0_hight ( * -1.0 repos_kid_5_hight ) ) 0.0 )
465 ( >= ( + repos_kid_0_hight ( * -1.0 repos_kid_5_hight ) ) 0.0 )
466 ( <= ( + repos_kid_0_hight ( * -1.0 repos_kid_6_hight ) ) 0.0 )
467 ( >= ( + repos_kid_0_hight ( * -1.0 repos_kid_6_hight ) ) 0.0 )
468 ( <= show_more_hight 50.0 )
469 ( >= show_more_hight 50.0 )
470 ( <= show_more_width 100.0 )
471 ( >= show_more_width 100.0 )
472 ( >= home_collom_holder_x 0.0 )
473 ( >= home_collom_holder_y 0.0 )
474 ( >= home_collom_holder_width 0.0 )
475 ( >= home_collom_holder_hight 0.0 )
476 home_collom_feasible
477 ( <= ( + home_collom_x ( * -1.0 home_collom_holder_x ) ) 0.0 )
478 ( >= ( + home_collom_width home_collom_x ( * -1.0 home_collom_holder_x ) ( * -1.0 home_collom_holder_width ) ) 0.0 )
479 ( >= ( + home_collom_holder_y ( * -1.0 home_collom_y ) ) 0.0 )
480 ( <= ( + home_collom_holder_y ( * -1.0 home_collom_y ) home_collom_holder_hight ( * -1.0 home_collom_hight ) ) 0.0 )
481 ( >= right_2_collom_x 0.0 )
482 ( >= right_2_collom_y 0.0 )
483 ( >= right_2_collom_width 0.0 )
484 ( >= right_2_collom_hight 0.0 )
485 ( >= right_1_collom_x 0.0 )
486 ( >= right_1_collom_y 0.0 )
487 ( >= right_1_collom_width 0.0 )
488 ( >= right_1_collom_hight 0.0 )
489 right_2_collom_feasible
490 ( <= ( + right_2_collom_x ( * -1.0 home_collom_holder_x ) ) 0.0 )
491 ( >= ( + right_2_collom_x ( * -1.0 home_collom_holder_x ) ) 0.0 )
492 ( <= ( + right_2_collom_x right_2_collom_width ( * -1.0 home_collom_holder_x ) ( * -1.0 home_collom_holder_width ) ) 0.0 )
493 ( >= ( + right_2_collom_x right_2_collom_width ( * -1.0 home_collom_holder_x ) ( * -1.0 home_collom_holder_width ) ) 0.0 )
494 ( <= ( + right_2_collom_y ( * -1.0 home_collom_holder_y ) ) 0.0 )
495 ( >= ( + right_2_collom_y ( * -1.0 home_collom_holder_y ) ) 0.0 )
496 ( <= ( + right_2_collom_y right_2_collom_hight ( * -1.0 home_collom_holder_y ) ( * -1.0 home_collom_holder_hight ) ) 0.0 )
497 ( >= ( + right_2_collom_y right_2_collom_hight ( * -1.0 home_collom_holder_y ) ( * -1.0 home_collom_holder_hight ) ) 0.0 )
498 right_1_collom_feasible
499 ( <= ( + right_1_collom_x ( * -1.0 home_collom_holder_x ) ) 0.0 )
500 ( >= ( + right_1_collom_x ( * -1.0 home_collom_holder_x ) ) 0.0 )
501 ( <= ( + right_1_collom_x right_1_collom_width ( * -1.0 home_collom_holder_x ) ( * -1.0 home_collom_holder_width ) ) 0.0 )
502 ( >= ( + right_1_collom_x right_1_collom_width ( * -1.0 home_collom_holder_x ) ( * -1.0 home_collom_holder_width ) ) 0.0 )
503 ( <= ( + right_1_collom_y ( * -1.0 home_collom_holder_y ) ) 0.0 )
504 ( >= ( + right_1_collom_y ( * -1.0 home_collom_holder_y ) ) 0.0 )
505 ( <= ( + right_1_collom_y right_1_collom_hight ( * -1.0 home_collom_holder_y ) ( * -1.0 home_collom_holder_hight ) ) 0.0 )
506 ( >= ( + right_1_collom_y right_1_collom_hight ( * -1.0 home_collom_holder_y ) ( * -1.0 home_collom_holder_hight ) ) 0.0 )
507 home_collom_holder_feasible
508 ( <= ( + home_collom_width ( * 2.0 home_collom_x ) ( * -2.0 home_collom_holder_x ) ( * -1.0 home_collom_holder_width ) ) 0.0 )
509 ( >= ( + home_collom_width ( * 2.0 home_collom_x ) ( * -2.0 home_collom_holder_x ) ( * -1.0 home_collom_holder_width ) ) 0.0 )
510 ( <= ( + home_collom_holder_y ( * -1.0 home_collom_y ) ) 20.0 )
511 ( >= ( + home_collom_holder_y ( * -1.0 home_collom_y ) ) 20.0 )
512 ( >= left_homes_x 0.0 )
513 ( >= left_homes_y 0.0 )
514 ( >= left_homes_width 0.0 )
515 ( >= left_homes_hight 0.0 )
516 ( >= right_homes_x 0.0 )
517 ( >= right_homes_y 0.0 )
518 ( >= right_homes_hight 0.0 )
519 ( <= ( + left_homes_x left_homes_width ( * -1.0 right_homes_x ) ) -20.0 )
520 ( >= ( + left_homes_x left_homes_width ( * -1.0 right_homes_x ) ) -20.0 )
521 ( >= ( + left_homes_x ( * -1.0 right_2_collom_x ) ) 0.0 )
522 ( <= ( + left_homes_x left_homes_width ( * -1.0 right_2_collom_x ) ( * -1.0 right_2_collom_width ) ) 0.0 )
523 ( >= ( + left_homes_y ( * -1.0 right_2_collom_y ) ) 0.0 )
524 ( <= ( + left_homes_y left_homes_hight ( * -1.0 right_2_collom_y ) ( * -1.0 right_2_collom_hight ) ) 0.0 )
525 ( <= ( + right_2_collom_x ( * -1.0 right_homes_x ) ) 0.0 )
526 ( <= ( + right_homes_y ( * -1.0 right_2_collom_y ) right_homes_hight ( * -1.0 right_2_collom_hight ) ) 0.0 )
527 ( <= ( + left_homes_x left_homes_width ( * -1.0 right_homes_x ) ) 0.0 )
528 ( <= home_collom_width 1000.0 )
529 ( <= right_2_collom_width 1000.0 )
530 ( >= right_2_collom_width 1000.0 )
531 ( <= ( + home_collom_width ( * -1.0 right_2_collom_width ) ) 20.0 )
532 ( >= ( + home_collom_width ( * -1.0 right_2_collom_width ) ) 20.0 )
533 ( >= home_title_x 0.0 )
534 ( >= home_title_y 0.0 )
535 ( >= home_title_width 0.0 )
536 ( >= z3_page_x 0.0 )
537 ( >= z3_page_y 0.0 )
538 ( >= z3_page_width 0.0 )
539 ( >= z3_page_hight 0.0 )
540 ( >= cvc_page_x 0.0 )
541 ( >= cvc_page_y 0.0 )
542 ( >= cvc_page_width 0.0 )
543 ( >= cvc_page_hight 0.0 )
544 ( >= rec_x 0.0 )
545 ( >= rec_y 0.0 )
546 ( >= rec_width 0.0 )
547 ( >= rec_hight 0.0 )
548 left_homes_feasible
549 ( <= ( + left_homes_x ( * -1.0 home_title_x ) ) 0.0 )
550 ( >= ( + left_homes_x ( * -1.0 home_title_x ) ) 0.0 )
551 ( <= ( + left_homes_x ( * -1.0 z3_page_x ) ) 0.0 )
552 ( >= ( + left_homes_x ( * -1.0 z3_page_x ) ) 0.0 )
553 ( <= ( + left_homes_x ( * -1.0 cvc_page_x ) ) 0.0 )
554 ( >= ( + left_homes_x ( * -1.0 cvc_page_x ) ) 0.0 )
555 ( <= ( + left_homes_x ( * -1.0 rec_x ) ) 0.0 )
556 ( >= ( + left_homes_x ( * -1.0 rec_x ) ) 0.0 )
557 ( <= ( + left_homes_x left_homes_width ( * -1.0 home_title_x ) ( * -1.0 home_title_width ) ) 0.0 )
558 ( >= ( + left_homes_x left_homes_width ( * -1.0 home_title_x ) ( * -1.0 home_title_width ) ) 0.0 )
559 ( <= ( + left_homes_x left_homes_width ( * -1.0 z3_page_x ) ( * -1.0 z3_page_width ) ) 0.0 )
560 ( >= ( + left_homes_x left_homes_width ( * -1.0 z3_page_x ) ( * -1.0 z3_page_width ) ) 0.0 )
561 ( <= ( + left_homes_x left_homes_width ( * -1.0 cvc_page_x ) ( * -1.0 cvc_page_width ) ) 0.0 )
562 ( >= ( + left_homes_x left_homes_width ( * -1.0 cvc_page_x ) ( * -1.0 cvc_page_width ) ) 0.0 )
563 ( <= ( + left_homes_x left_homes_width ( * -1.0 rec_x ) ( * -1.0 rec_width ) ) 0.0 )
564 ( >= ( + left_homes_x left_homes_width ( * -1.0 rec_x ) ( * -1.0 rec_width ) ) 0.0 )
565 ( <= ( + left_homes_y ( * -1.0 home_title_y ) ) 0.0 )
566 ( >= ( + left_homes_y ( * -1.0 home_title_y ) ) 0.0 )
567 ( <= ( + left_homes_y left_homes_hight ( * -1.0 rec_hight ) ( * -1.0 rec_y ) ) 0.0 )
568 ( >= ( + left_homes_y left_homes_hight ( * -1.0 rec_hight ) ( * -1.0 rec_y ) ) 0.0 )
569 ( <= ( + z3_page_y ( * -1.0 home_title_y ) ) 70.0 )
570 ( >= ( + z3_page_y ( * -1.0 home_title_y ) ) 70.0 )
571 ( <= ( + cvc_page_y ( * -1.0 z3_page_y ) ( * -1.0 z3_page_hight ) ) 20.0 )
572 ( >= ( + cvc_page_y ( * -1.0 z3_page_y ) ( * -1.0 z3_page_hight ) ) 20.0 )
573 ( <= ( + rec_y ( * -1.0 cvc_page_y ) ( * -1.0 cvc_page_hight ) ) 20.0 )
574 ( >= ( + rec_y ( * -1.0 cvc_page_y ) ( * -1.0 cvc_page_hight ) ) 20.0 )
575 ( >= ( + left_homes_y left_homes_hight ( * -1.0 home_title_y ) ) 50.0 )
576 ( <= ( + left_homes_y ( * -1.0 z3_page_y ) ) 0.0 )
577 ( >= ( + left_homes_y left_homes_hight ( * -1.0 z3_page_y ) ( * -1.0 z3_page_hight ) ) 0.0 )
578 ( <= ( + left_homes_y ( * -1.0 cvc_page_y ) ) 0.0 )
579 ( >= ( + left_homes_y left_homes_hight ( * -1.0 cvc_page_y ) ( * -1.0 cvc_page_hight ) ) 0.0 )
580 ( <= ( + left_homes_y ( * -1.0 rec_y ) ) 0.0 )
581 ( >= ( + z3_page_y ( * -1.0 home_title_y ) ) 50.0 )
582 ( >= ( + cvc_page_y ( * -1.0 z3_page_y ) ( * -1.0 z3_page_hight ) ) 0.0 )
583 ( >= ( + rec_y ( * -1.0 cvc_page_y ) ( * -1.0 cvc_page_hight ) ) 0.0 )
584 ( <= ( + left_homes_x ( * -1.0 right_2_collom_x ) ) 0.0 )
585 ( <= left_homes_width 500.0 )
586 ( >= home_icon_x 0.0 )
587 ( >= home_icon_y 0.0 )
588 ( >= home_icon_width 0.0 )
589 ( >= home_icon_hight 0.0 )
590 ( >= send_feedback_x 0.0 )
591 ( >= send_feedback_y 0.0 )
592 ( >= send_feedback_width 0.0 )
593 ( >= send_feedback_hight 0.0 )
594 ( >= filter_x 0.0 )
595 ( >= filter_y 0.0 )
596 ( >= filter_width 0.0 )
597 ( >= filter_hight 0.0 )
598 ( <= home_title_hight 50.0 )
599 ( >= home_title_hight 50.0 )
600 home_title_feasible
601 ( <= ( + home_icon_x ( * -1.0 home_title_x ) ) 0.0 )
602 ( >= ( + home_icon_x ( * -1.0 home_title_x ) ) 0.0 )
603 ( <= ( + filter_x ( * -1.0 home_title_x ) filter_width ( * -1.0 home_title_width ) ) 0.0 )
604 ( >= ( + filter_x ( * -1.0 home_title_x ) filter_width ( * -1.0 home_title_width ) ) 0.0 )
605 ( <= ( + home_title_y ( * -1.0 home_icon_y ) ) 0.0 )
606 ( >= ( + home_title_y ( * -1.0 home_icon_y ) ) 0.0 )
607 ( <= ( + home_title_y ( * -1.0 send_feedback_y ) ) 0.0 )
608 ( >= ( + home_title_y ( * -1.0 send_feedback_y ) ) 0.0 )
609 ( <= ( + home_title_y ( * -1.0 filter_y ) ) 0.0 )
610 ( >= ( + home_title_y ( * -1.0 filter_y ) ) 0.0 )
611 ( <= ( + home_title_y ( * -1.0 home_icon_y ) ( * -1.0 home_icon_hight ) ) -50.0 )
612 ( >= ( + home_title_y ( * -1.0 home_icon_y ) ( * -1.0 home_icon_hight ) ) -50.0 )
613 ( <= ( + home_title_y ( * -1.0 send_feedback_y ) ( * -1.0 send_feedback_hight ) ) -50.0 )
614 ( >= ( + home_title_y ( * -1.0 send_feedback_y ) ( * -1.0 send_feedback_hight ) ) -50.0 )
615 ( <= ( + home_title_y ( * -1.0 filter_y ) ( * -1.0 filter_hight ) ) -50.0 )
616 ( >= ( + home_title_y ( * -1.0 filter_y ) ( * -1.0 filter_hight ) ) -50.0 )
617 ( <= ( + home_icon_x ( * -1.0 home_title_x ) home_icon_width ( * -1.0 home_title_width ) ) 0.0 )
618 ( >= ( + send_feedback_x ( * -1.0 home_title_x ) ) 0.0 )
619 ( <= ( + send_feedback_x send_feedback_width ( * -1.0 home_title_x ) ( * -1.0 home_title_width ) ) 0.0 )
620 ( >= ( + filter_x ( * -1.0 home_title_x ) ) 0.0 )
621 ( >= ( + send_feedback_x ( * -1.0 home_icon_x ) ( * -1.0 home_icon_width ) ) 0.0 )
622 ( <= ( + send_feedback_x send_feedback_width ( * -1.0 filter_x ) ) 0.0 )
623 ( <= ( + send_feedback_width ( * -1.0 home_icon_width ) ) 0.0 )
624 ( >= ( + send_feedback_width ( * -1.0 home_icon_width ) ) 0.0 )
625 ( <= ( + home_icon_width ( * -1.0 filter_width ) ) 0.0 )
626 ( >= ( + home_icon_width ( * -1.0 filter_width ) ) 0.0 )
627 ( <= home_icon_width 100.0 )
628 ( >= home_icon_width 100.0 )
629 ( <= ( + send_feedback_x send_feedback_width ( * -1.0 filter_x ) ) -10.0 )
630 ( >= ( + send_feedback_x send_feedback_width ( * -1.0 filter_x ) ) -10.0 )
631 ( >= z3_icon_x 0.0 )
632 ( >= z3_icon_y 0.0 )
633 ( >= z3_version_x 0.0 )
634 ( >= z3_version_y 0.0 )
635 ( >= changes_x 0.0 )
636 ( >= changes_y 0.0 )
637 ( >= changes_width 0.0 )
638 ( >= z3_smile_x 0.0 )
639 ( >= z3_smile_y 0.0 )
640 z3_page_feasible
641 ( <= ( + z3_icon_y ( * -1.0 z3_version_y ) ) -70.0 )
642 ( >= ( + z3_icon_y ( * -1.0 z3_version_y ) ) -70.0 )
643 ( <= ( + changes_y ( * -1.0 z3_version_y ) ) 70.0 )
644 ( >= ( + changes_y ( * -1.0 z3_version_y ) ) 70.0 )
645 ( <= ( + z3_smile_y ( * -1.0 changes_y ) ) 220.0 )
646 ( >= ( + z3_smile_y ( * -1.0 changes_y ) ) 220.0 )
647 ( <= ( + z3_page_x ( * -1.0 z3_icon_x ) ) -20.0 )
648 ( >= ( + z3_page_x z3_page_width ( * -1.0 z3_icon_x ) ) 70.0 )
649 ( <= ( + z3_page_y ( * -1.0 z3_icon_y ) ) -20.0 )
650 ( >= ( + z3_page_y ( * -1.0 z3_icon_y ) z3_page_hight ) 70.0 )
651 ( <= ( + z3_page_x ( * -1.0 z3_version_x ) ) -20.0 )
652 ( >= ( + z3_page_x z3_page_width ( * -1.0 z3_version_x ) ) 120.0 )
653 ( <= ( + z3_page_y ( * -1.0 z3_version_y ) ) -20.0 )
654 ( >= ( + z3_page_y z3_page_hight ( * -1.0 z3_version_y ) ) 70.0 )
655 ( <= ( + z3_page_x ( * -1.0 changes_x ) ) -20.0 )
656 ( >= ( + z3_page_x ( * -1.0 changes_x ) ( * -1.0 changes_width ) z3_page_width ) 20.0 )
657 ( <= ( + z3_page_y ( * -1.0 changes_y ) ) -20.0 )
658 ( >= ( + z3_page_y z3_page_hight ( * -1.0 changes_y ) ) 220.0 )
659 ( <= ( + z3_page_x ( * -1.0 z3_smile_x ) ) -20.0 )
660 ( >= ( + z3_page_x z3_page_width ( * -1.0 z3_smile_x ) ) 70.0 )
661 ( <= ( + z3_page_y ( * -1.0 z3_smile_y ) ) -20.0 )
662 ( >= ( + z3_page_y z3_page_hight ( * -1.0 z3_smile_y ) ) 70.0 )
663 ( <= ( + z3_icon_y ( * -1.0 z3_version_y ) ) -50.0 )
664 ( >= ( + changes_y ( * -1.0 z3_version_y ) ) 50.0 )
665 ( >= ( + z3_smile_y ( * -1.0 changes_y ) ) 200.0 )
666 ( >= ( + z3_page_x ( * -1.0 z3_icon_x ) ) -20.0 )
667 ( >= ( + z3_page_x ( * -1.0 z3_version_x ) ) -20.0 )
668 ( >= ( + z3_page_x ( * -1.0 changes_x ) ) -20.0 )
669 ( >= ( + z3_page_x ( * -1.0 z3_smile_x ) ) -20.0 )
670 ( <= z3_icon_width 50.0 )
671 ( >= z3_icon_width 50.0 )
672 ( <= z3_icon_hight 50.0 )
673 ( >= z3_icon_hight 50.0 )
674 ( <= z3_version_width 100.0 )
675 ( >= z3_version_width 100.0 )
676 ( <= z3_version_hight 50.0 )
677 ( >= z3_version_hight 50.0 )
678 ( <= changes_hight 200.0 )
679 ( >= changes_hight 200.0 )
680 ( <= ( + z3_page_x ( * -1.0 changes_x ) ( * -1.0 changes_width ) z3_page_width ) 20.0 )
681 ( <= ( + z3_page_y z3_page_hight ( * -1.0 z3_smile_y ) ) 70.0 )
682 ( <= z3_smile_width 50.0 )
683 ( >= z3_smile_width 50.0 )
684 ( <= z3_smile_hight 50.0 )
685 ( >= z3_smile_hight 50.0 )
686 ( >= ( + z3_page_y ( * -1.0 z3_icon_y ) ) -20.0 )
687 ( >= cvc_icon_x 0.0 )
688 ( >= cvc_icon_y 0.0 )
689 ( >= cvc_version_x 0.0 )
690 ( >= cvc_version_y 0.0 )
691 ( >= cvc_changes_x 0.0 )
692 ( >= cvc_changes_y 0.0 )
693 ( >= cvc_changes_width 0.0 )
694 ( >= cvc_smile_x 0.0 )
695 ( >= cvc_smile_y 0.0 )
696 cvc_page_feasible
697 ( <= ( + cvc_icon_y ( * -1.0 cvc_version_y ) ) -70.0 )
698 ( >= ( + cvc_icon_y ( * -1.0 cvc_version_y ) ) -70.0 )
699 ( <= ( + cvc_changes_y ( * -1.0 cvc_version_y ) ) 70.0 )
700 ( >= ( + cvc_changes_y ( * -1.0 cvc_version_y ) ) 70.0 )
701 ( <= ( + cvc_smile_y ( * -1.0 cvc_changes_y ) ) 220.0 )
702 ( >= ( + cvc_smile_y ( * -1.0 cvc_changes_y ) ) 220.0 )
703 ( <= ( + cvc_page_x ( * -1.0 cvc_icon_x ) ) -20.0 )
704 ( >= ( + cvc_page_x cvc_page_width ( * -1.0 cvc_icon_x ) ) 170.0 )
705 ( <= ( + cvc_page_y ( * -1.0 cvc_icon_y ) ) -20.0 )
706 ( >= ( + cvc_page_y ( * -1.0 cvc_icon_y ) cvc_page_hight ) 70.0 )
707 ( <= ( + cvc_page_x ( * -1.0 cvc_version_x ) ) -20.0 )
708 ( >= ( + cvc_page_x cvc_page_width ( * -1.0 cvc_version_x ) ) 120.0 )
709 ( <= ( + cvc_page_y ( * -1.0 cvc_version_y ) ) -20.0 )
710 ( >= ( + cvc_page_y cvc_page_hight ( * -1.0 cvc_version_y ) ) 70.0 )
711 ( <= ( + cvc_page_x ( * -1.0 cvc_changes_x ) ) -20.0 )
712 ( <= ( + cvc_changes_width ( * -1.0 cvc_page_x ) ( * -1.0 cvc_page_width ) cvc_changes_x ) -20.0 )
713 ( <= ( + cvc_page_y ( * -1.0 cvc_changes_y ) ) -20.0 )
714 ( >= ( + cvc_page_y cvc_page_hight ( * -1.0 cvc_changes_y ) ) 220.0 )
715 ( <= ( + cvc_page_x ( * -1.0 cvc_smile_x ) ) -20.0 )
716 ( >= ( + cvc_page_x cvc_page_width ( * -1.0 cvc_smile_x ) ) 70.0 )
717 ( <= ( + cvc_page_y ( * -1.0 cvc_smile_y ) ) -20.0 )
718 ( >= ( + cvc_page_y ( * -1.0 cvc_smile_y ) cvc_page_hight ) 70.0 )
719 ( <= ( + cvc_icon_y ( * -1.0 cvc_version_y ) ) -50.0 )
720 ( >= ( + cvc_changes_y ( * -1.0 cvc_version_y ) ) 50.0 )
721 ( >= ( + cvc_smile_y ( * -1.0 cvc_changes_y ) ) 200.0 )
722 ( >= ( + cvc_page_x ( * -1.0 cvc_icon_x ) ) -20.0 )
723 ( >= ( + cvc_page_x ( * -1.0 cvc_version_x ) ) -20.0 )
724 ( >= ( + cvc_page_x ( * -1.0 cvc_changes_x ) ) -20.0 )
725 ( >= ( + cvc_page_x ( * -1.0 cvc_smile_x ) ) -20.0 )
726 ( <= cvc_icon_width 150.0 )
727 ( >= cvc_icon_width 150.0 )
728 ( <= cvc_icon_hight 50.0 )
729 ( >= cvc_icon_hight 50.0 )
730 ( <= cvc_version_width 100.0 )
731 ( >= cvc_version_width 100.0 )
732 ( <= cvc_version_hight 50.0 )
733 ( >= cvc_version_hight 50.0 )
734 ( <= cvc_changes_hight 200.0 )
735 ( >= cvc_changes_hight 200.0 )
736 ( >= ( + cvc_changes_width ( * -1.0 cvc_page_x ) ( * -1.0 cvc_page_width ) cvc_changes_x ) -20.0 )
737 ( <= ( + cvc_page_y ( * -1.0 cvc_smile_y ) cvc_page_hight ) 70.0 )
738 ( <= cvc_smile_width 50.0 )
739 ( >= cvc_smile_width 50.0 )
740 ( <= cvc_smile_hight 50.0 )
741 ( >= cvc_smile_hight 50.0 )
742 ( >= ( + cvc_page_y ( * -1.0 cvc_icon_y ) ) -20.0 )
743 ( >= recomend_for_you_x 0.0 )
744 ( >= recomend_for_you_y 0.0 )
745 rec_feasible
746 ( <= ( + rec_x ( * -1.0 recomend_for_you_x ) ) -20.0 )
747 ( >= ( + rec_x ( * -1.0 recomend_for_you_x ) ) -20.0 )
748 ( <= ( + rec_y ( * -1.0 recomend_for_you_y ) ) -20.0 )
749 ( >= ( + rec_y ( * -1.0 recomend_for_you_y ) ) -20.0 )
750 ( <= recomend_for_you_width 100.0 )
751 ( >= recomend_for_you_width 100.0 )
752 ( <= recomend_for_you_hight 50.0 )
753 ( >= recomend_for_you_hight 50.0 )
754 ( >= boolect_x 0.0 )
755 ( >= boolect_y 0.0 )
756 ( <= boolect_width 100.0 )
757 ( >= boolect_width 100.0 )
758 ( <= boolect_hight 50.0 )
759 ( >= boolect_hight 50.0 )
760 ( <= ( + rec_x ( * -1.0 boolect_x ) ) -20.0 )
761 ( >= ( + rec_x ( * -1.0 boolect_x ) ) -20.0 )
762 ( <= ( + boolect_y ( * -1.0 recomend_for_you_y ) ) 70.0 )
763 ( >= ( + boolect_y ( * -1.0 recomend_for_you_y ) ) 70.0 )
764 ( >= stars_x 0.0 )
765 ( >= stars_y 0.0 )
766 ( >= stars_hight 0.0 )
767 ( <= ( + rec_x rec_width ( * -1.0 stars_x ) ) 120.0 )
768 ( >= ( + rec_x rec_width ( * -1.0 stars_x ) ) 120.0 )
769 ( <= ( + boolect_y ( * -1.0 stars_y ) ) 0.0 )
770 ( >= ( + boolect_y ( * -1.0 stars_y ) ) 0.0 )
771 ( <= stars_hight 50.0 )
772 ( >= stars_hight 50.0 )
773 ( <= stars_width 100.0 )
774 ( >= stars_width 100.0 )
775 ( >= rec_word_x 0.0 )
776 ( >= rec_word_y 0.0 )
777 ( >= rec_word_width 0.0 )
778 ( <= ( + rec_x ( * -1.0 rec_word_x ) ) -20.0 )
779 ( >= ( + rec_x ( * -1.0 rec_word_x ) ) -20.0 )
780 ( <= ( + rec_x ( * -1.0 rec_word_x ) ( * -1.0 rec_word_width ) rec_width ) 20.0 )
781 ( >= ( + rec_x ( * -1.0 rec_word_x ) ( * -1.0 rec_word_width ) rec_width ) 20.0 )
782 ( <= rec_word_hight 200.0 )
783 ( >= rec_word_hight 200.0 )
784 ( <= ( + rec_word_y ( * -1.0 boolect_y ) ) 70.0 )
785 ( >= ( + rec_word_y ( * -1.0 boolect_y ) ) 70.0 )
786 ( >= rec_left_icon_x 0.0 )
787 ( >= rec_left_icon_y 0.0 )
788 ( <= ( + rec_left_icon_x ( * -1.0 rec_x ) ) 20.0 )
789 ( >= ( + rec_left_icon_x ( * -1.0 rec_x ) ) 20.0 )
790 ( <= ( + rec_word_y ( * -1.0 rec_left_icon_y ) ) -220.0 )
791 ( >= ( + rec_word_y ( * -1.0 rec_left_icon_y ) ) -220.0 )
792 ( <= rec_left_icon_width 50.0 )
793 ( >= rec_left_icon_width 50.0 )
794 ( <= rec_left_icon_hight 50.0 )
795 ( >= rec_left_icon_hight 50.0 )
796 ( >= rec_right_icon_x 0.0 )
797 ( >= rec_right_icon_y 0.0 )
798 ( <= ( + rec_left_icon_x ( * -1.0 rec_right_icon_x ) ) -70.0 )
799 ( >= ( + rec_left_icon_x ( * -1.0 rec_right_icon_x ) ) -70.0 )
800 ( <= ( + rec_right_icon_y ( * -1.0 rec_word_y ) ) 220.0 )
801 ( >= ( + rec_right_icon_y ( * -1.0 rec_word_y ) ) 220.0 )
802 ( <= rec_right_icon_width 50.0 )
803 ( >= rec_right_icon_width 50.0 )
804 ( <= rec_right_icon_hight 50.0 )
805 ( >= rec_right_icon_hight 50.0 )
806 ( <= ( + rec_hight ( * -1.0 rec_right_icon_y ) rec_y ) 70.0 )
807 ( >= ( + rec_hight ( * -1.0 rec_right_icon_y ) rec_y ) 70.0 )
808 ( >= last_changes_x 0.0 )
809 ( >= last_changes_y 0.0 )
810 ( >= last_changes_width 0.0 )
811 ( >= last_changes_hight 0.0 )
812 ( >= explore_repo_x 0.0 )
813 ( >= explore_repo_y 0.0 )
814 ( >= explore_repo_width 0.0 )
815 ( >= explore_repo_hight 0.0 )
816 right_homes_feasible
817 ( <= ( + last_changes_x ( * -1.0 right_homes_x ) ) 0.0 )
818 ( >= ( + last_changes_x ( * -1.0 right_homes_x ) ) 0.0 )
819 ( <= ( + explore_repo_x ( * -1.0 right_homes_x ) ) 0.0 )
820 ( >= ( + explore_repo_x ( * -1.0 right_homes_x ) ) 0.0 )
821 ( <= ( + last_changes_x last_changes_width ( * -1.0 right_homes_x ) ) 400.0 )
822 ( >= ( + last_changes_x last_changes_width ( * -1.0 right_homes_x ) ) 400.0 )
823 ( <= ( + explore_repo_x explore_repo_width ( * -1.0 right_homes_x ) ) 400.0 )
824 ( >= ( + explore_repo_x explore_repo_width ( * -1.0 right_homes_x ) ) 400.0 )
825 ( <= ( + last_changes_y ( * -1.0 right_homes_y ) ) 0.0 )
826 ( >= ( + last_changes_y ( * -1.0 right_homes_y ) ) 0.0 )
827 ( <= ( + explore_repo_hight explore_repo_y ( * -1.0 right_homes_y ) ( * -1.0 right_homes_hight ) ) 0.0 )
828 ( >= ( + explore_repo_hight explore_repo_y ( * -1.0 right_homes_y ) ( * -1.0 right_homes_hight ) ) 0.0 )
829 ( <= ( + last_changes_y last_changes_hight ( * -1.0 right_homes_y ) ( * -1.0 right_homes_hight ) ) 0.0 )
830 ( >= ( + explore_repo_y ( * -1.0 right_homes_y ) ) 0.0 )
831 ( >= ( + explore_repo_y ( * -1.0 last_changes_y ) ( * -1.0 last_changes_hight ) ) 0.0 )
832 ( <= ( + explore_repo_y ( * -1.0 last_changes_y ) ( * -1.0 last_changes_hight ) ) 20.0 )
833 ( >= ( + explore_repo_y ( * -1.0 last_changes_y ) ( * -1.0 last_changes_hight ) ) 20.0 )
834 ( <= right_homes_width 400.0 )
835 ( >= right_homes_width 400.0 )
836 ( <= ( + right_homes_width ( * -1.0 right_2_collom_x ) ( * -1.0 right_2_collom_width ) right_homes_x ) 0.0 )
837 ( >= ( + right_homes_width ( * -1.0 right_2_collom_x ) ( * -1.0 right_2_collom_width ) right_homes_x ) 0.0 )
838 ( <= ( + right_homes_y ( * -1.0 right_2_collom_y ) ) 0.0 )
839 ( >= ( + right_homes_y ( * -1.0 right_2_collom_y ) ) 0.0 )
840 ( >= last_changes_title_x 0.0 )
841 ( >= last_changes_title_y 0.0 )
842 ( >= last_changes_title_width 0.0 )
843 ( >= last_changes_title_hight 0.0 )
844 ( >= last_changes_body_x 0.0 )
845 ( >= last_changes_body_y 0.0 )
846 ( >= last_changes_body_width 0.0 )
847 ( >= last_changes_body_hight 0.0 )
848 last_changes_feasible
849 ( <= ( + last_changes_x ( * -1.0 last_changes_title_x ) ) 0.0 )
850 ( >= ( + last_changes_x last_changes_width ( * -1.0 last_changes_title_x ) ( * -1.0 last_changes_title_width ) ) 0.0 )
851 ( >= ( + last_changes_title_y ( * -1.0 last_changes_y ) ) 0.0 )
852 ( <= ( + last_changes_title_hight last_changes_title_y ( * -1.0 last_changes_y ) ( * -1.0 last_changes_hight ) ) 0.0 )
853 ( >= ( + last_changes_body_x ( * -1.0 last_changes_x ) ) 0.0 )
854 ( <= ( + last_changes_body_x last_changes_body_width ( * -1.0 last_changes_x ) ( * -1.0 last_changes_width ) ) 0.0 )
855 ( >= ( + last_changes_body_y ( * -1.0 last_changes_y ) ) 0.0 )
856 ( <= ( + last_changes_body_hight last_changes_body_y ( * -1.0 last_changes_y ) ( * -1.0 last_changes_hight ) ) 0.0 )
857 ( >= ( + last_changes_body_y ( * -1.0 last_changes_title_hight ) ( * -1.0 last_changes_title_y ) ) 0.0 )
858 ( <= ( + last_changes_x ( * -1.0 last_changes_title_x ) ) -20.0 )
859 ( >= ( + last_changes_x ( * -1.0 last_changes_title_x ) ) -20.0 )
860 ( <= ( + last_changes_body_x ( * -1.0 last_changes_x ) ) 20.0 )
861 ( >= ( + last_changes_body_x ( * -1.0 last_changes_x ) ) 20.0 )
862 ( <= ( + last_changes_x last_changes_width ( * -1.0 last_changes_title_x ) ( * -1.0 last_changes_title_width ) ) 20.0 )
863 ( >= ( + last_changes_x last_changes_width ( * -1.0 last_changes_title_x ) ( * -1.0 last_changes_title_width ) ) 20.0 )
864 ( <= ( + last_changes_body_x last_changes_body_width ( * -1.0 last_changes_x ) ( * -1.0 last_changes_width ) ) -20.0 )
865 ( >= ( + last_changes_body_x last_changes_body_width ( * -1.0 last_changes_x ) ( * -1.0 last_changes_width ) ) -20.0 )
866 ( <= ( + last_changes_title_y ( * -1.0 last_changes_y ) ) 20.0 )
867 ( >= ( + last_changes_title_y ( * -1.0 last_changes_y ) ) 20.0 )
868 ( <= ( + last_changes_body_hight last_changes_body_y ( * -1.0 last_changes_y ) ( * -1.0 last_changes_hight ) ) -20.0 )
869 ( >= ( + last_changes_body_hight last_changes_body_y ( * -1.0 last_changes_y ) ( * -1.0 last_changes_hight ) ) -20.0 )
870 ( <= ( + last_changes_body_y ( * -1.0 last_changes_title_hight ) ( * -1.0 last_changes_title_y ) ) 20.0 )
871 ( >= ( + last_changes_body_y ( * -1.0 last_changes_title_hight ) ( * -1.0 last_changes_title_y ) ) 20.0 )
872 ( <= last_changes_title_hight 50.0 )
873 ( >= last_changes_title_hight 50.0 )
874 ( >= last_changes_body_kid_0_x 0.0 )
875 ( >= last_changes_body_kid_0_y 0.0 )
876 ( >= last_changes_body_kid_1_x 0.0 )
877 ( >= last_changes_body_kid_1_y 0.0 )
878 ( >= last_changes_body_kid_2_x 0.0 )
879 ( >= last_changes_body_kid_2_y 0.0 )
880 ( >= last_changes_body_kid_3_x 0.0 )
881 ( >= last_changes_body_kid_3_y 0.0 )
882 ( >= last_changes_body_kid_4_x 0.0 )
883 ( >= last_changes_body_kid_4_y 0.0 )
884 ( >= last_changes_body_kid_5_x 0.0 )
885 ( >= last_changes_body_kid_5_y 0.0 )
886 ( >= last_changes_body_kid_6_x 0.0 )
887 ( >= last_changes_body_kid_6_y 0.0 )
888 ( >= last_changes_body_kid_7_x 0.0 )
889 ( >= last_changes_body_kid_7_y 0.0 )
890 ( >= last_changes_body_kid_8_x 0.0 )
891 ( >= last_changes_body_kid_8_y 0.0 )
892 last_changes_body_feasible
893 ( <= ( + last_changes_body_x ( * -1.0 last_changes_body_kid_0_x ) ) -20.0 )
894 ( >= ( + last_changes_body_x ( * -1.0 last_changes_body_kid_0_x ) last_changes_body_width ) 120.0 )
895 ( >= ( + last_changes_body_kid_0_y ( * -1.0 last_changes_body_y ) ) 20.0 )
896 ( <= ( + last_changes_body_kid_0_y ( * -1.0 last_changes_body_hight ) ( * -1.0 last_changes_body_y ) ) -50.0 )
897 ( <= ( + last_changes_body_x ( * -1.0 last_changes_body_kid_1_x ) ) -20.0 )
898 ( >= ( + last_changes_body_x ( * -1.0 last_changes_body_kid_1_x ) last_changes_body_width ) 320.0 )
899 ( >= ( + last_changes_body_kid_1_y ( * -1.0 last_changes_body_y ) ) 20.0 )
900 ( <= ( + last_changes_body_kid_1_y ( * -1.0 last_changes_body_hight ) ( * -1.0 last_changes_body_y ) ) -70.0 )
901 ( <= ( + last_changes_body_x ( * -1.0 last_changes_body_kid_2_x ) ) -20.0 )
902 ( >= ( + last_changes_body_x ( * -1.0 last_changes_body_kid_2_x ) last_changes_body_width ) 120.0 )
903 ( >= ( + last_changes_body_kid_2_y ( * -1.0 last_changes_body_y ) ) 20.0 )
904 ( <= ( + last_changes_body_kid_2_y ( * -1.0 last_changes_body_hight ) ( * -1.0 last_changes_body_y ) ) -50.0 )
905 ( <= ( + last_changes_body_x ( * -1.0 last_changes_body_kid_3_x ) ) -20.0 )
906 ( >= ( + last_changes_body_x ( * -1.0 last_changes_body_kid_3_x ) last_changes_body_width ) 320.0 )
907 ( >= ( + last_changes_body_kid_3_y ( * -1.0 last_changes_body_y ) ) 20.0 )
908 ( <= ( + last_changes_body_kid_3_y ( * -1.0 last_changes_body_hight ) ( * -1.0 last_changes_body_y ) ) -70.0 )
909 ( <= ( + last_changes_body_x ( * -1.0 last_changes_body_kid_4_x ) ) -20.0 )
910 ( >= ( + last_changes_body_x ( * -1.0 last_changes_body_kid_4_x ) last_changes_body_width ) 120.0 )
911 ( >= ( + last_changes_body_kid_4_y ( * -1.0 last_changes_body_y ) ) 20.0 )
912 ( <= ( + last_changes_body_kid_4_y ( * -1.0 last_changes_body_hight ) ( * -1.0 last_changes_body_y ) ) -50.0 )
913 ( <= ( + last_changes_body_x ( * -1.0 last_changes_body_kid_5_x ) ) -20.0 )
914 ( >= ( + last_changes_body_x ( * -1.0 last_changes_body_kid_5_x ) last_changes_body_width ) 320.0 )
915 ( >= ( + last_changes_body_kid_5_y ( * -1.0 last_changes_body_y ) ) 20.0 )
916 ( <= ( + last_changes_body_kid_5_y ( * -1.0 last_changes_body_hight ) ( * -1.0 last_changes_body_y ) ) -70.0 )
917 ( <= ( + last_changes_body_x ( * -1.0 last_changes_body_kid_6_x ) ) -20.0 )
918 ( >= ( + last_changes_body_x ( * -1.0 last_changes_body_kid_6_x ) last_changes_body_width ) 120.0 )
919 ( >= ( + last_changes_body_kid_6_y ( * -1.0 last_changes_body_y ) ) 20.0 )
920 ( <= ( + last_changes_body_kid_6_y ( * -1.0 last_changes_body_hight ) ( * -1.0 last_changes_body_y ) ) -50.0 )
921 ( <= ( + last_changes_body_x ( * -1.0 last_changes_body_kid_7_x ) ) -20.0 )
922 ( >= ( + last_changes_body_x ( * -1.0 last_changes_body_kid_7_x ) last_changes_body_width ) 320.0 )
923 ( >= ( + last_changes_body_kid_7_y ( * -1.0 last_changes_body_y ) ) 20.0 )
924 ( <= ( + last_changes_body_kid_7_y ( * -1.0 last_changes_body_hight ) ( * -1.0 last_changes_body_y ) ) -70.0 )
925 ( <= ( + last_changes_body_x ( * -1.0 last_changes_body_kid_8_x ) ) -20.0 )
926 ( >= ( + last_changes_body_x ( * -1.0 last_changes_body_kid_8_x ) last_changes_body_width ) 120.0 )
927 ( >= ( + last_changes_body_kid_8_y ( * -1.0 last_changes_body_y ) ) 20.0 )
928 ( <= ( + last_changes_body_kid_8_y ( * -1.0 last_changes_body_hight ) ( * -1.0 last_changes_body_y ) ) -50.0 )
929 ( >= ( + last_changes_body_kid_1_y ( * -1.0 last_changes_body_kid_0_y ) ) 30.0 )
930 ( >= ( + last_changes_body_kid_2_y ( * -1.0 last_changes_body_kid_1_y ) ) 50.0 )
931 ( >= ( + last_changes_body_kid_3_y ( * -1.0 last_changes_body_kid_2_y ) ) 30.0 )
932 ( >= ( + last_changes_body_kid_4_y ( * -1.0 last_changes_body_kid_3_y ) ) 50.0 )
933 ( >= ( + last_changes_body_kid_5_y ( * -1.0 last_changes_body_kid_4_y ) ) 30.0 )
934 ( >= ( + last_changes_body_kid_6_y ( * -1.0 last_changes_body_kid_5_y ) ) 50.0 )
935 ( >= ( + last_changes_body_kid_7_y ( * -1.0 last_changes_body_kid_6_y ) ) 30.0 )
936 ( >= ( + last_changes_body_kid_8_y ( * -1.0 last_changes_body_kid_7_y ) ) 50.0 )
937 ( >= ( + last_changes_body_x ( * -1.0 last_changes_body_kid_0_x ) ) -20.0 )
938 ( >= ( + last_changes_body_x ( * -1.0 last_changes_body_kid_1_x ) ) -20.0 )
939 ( >= ( + last_changes_body_x ( * -1.0 last_changes_body_kid_2_x ) ) -20.0 )
940 ( >= ( + last_changes_body_x ( * -1.0 last_changes_body_kid_3_x ) ) -20.0 )
941 ( >= ( + last_changes_body_x ( * -1.0 last_changes_body_kid_4_x ) ) -20.0 )
942 ( >= ( + last_changes_body_x ( * -1.0 last_changes_body_kid_5_x ) ) -20.0 )
943 ( >= ( + last_changes_body_x ( * -1.0 last_changes_body_kid_6_x ) ) -20.0 )
944 ( >= ( + last_changes_body_x ( * -1.0 last_changes_body_kid_7_x ) ) -20.0 )
945 ( >= ( + last_changes_body_x ( * -1.0 last_changes_body_kid_8_x ) ) -20.0 )
946 ( <= ( + last_changes_body_kid_1_y ( * -1.0 last_changes_body_kid_0_y ) ) 40.0 )
947 ( >= ( + last_changes_body_kid_1_y ( * -1.0 last_changes_body_kid_0_y ) ) 40.0 )
948 ( <= ( + last_changes_body_kid_2_y ( * -1.0 last_changes_body_kid_1_y ) ) 60.0 )
949 ( >= ( + last_changes_body_kid_2_y ( * -1.0 last_changes_body_kid_1_y ) ) 60.0 )
950 ( <= ( + last_changes_body_kid_3_y ( * -1.0 last_changes_body_kid_2_y ) ) 40.0 )
951 ( >= ( + last_changes_body_kid_3_y ( * -1.0 last_changes_body_kid_2_y ) ) 40.0 )
952 ( <= ( + last_changes_body_kid_4_y ( * -1.0 last_changes_body_kid_3_y ) ) 60.0 )
953 ( >= ( + last_changes_body_kid_4_y ( * -1.0 last_changes_body_kid_3_y ) ) 60.0 )
954 ( <= ( + last_changes_body_kid_5_y ( * -1.0 last_changes_body_kid_4_y ) ) 40.0 )
955 ( >= ( + last_changes_body_kid_5_y ( * -1.0 last_changes_body_kid_4_y ) ) 40.0 )
956 ( <= ( + last_changes_body_kid_6_y ( * -1.0 last_changes_body_kid_5_y ) ) 60.0 )
957 ( >= ( + last_changes_body_kid_6_y ( * -1.0 last_changes_body_kid_5_y ) ) 60.0 )
958 ( <= ( + last_changes_body_kid_7_y ( * -1.0 last_changes_body_kid_6_y ) ) 40.0 )
959 ( >= ( + last_changes_body_kid_7_y ( * -1.0 last_changes_body_kid_6_y ) ) 40.0 )
960 ( <= ( + last_changes_body_kid_8_y ( * -1.0 last_changes_body_kid_7_y ) ) 60.0 )
961 ( >= ( + last_changes_body_kid_8_y ( * -1.0 last_changes_body_kid_7_y ) ) 60.0 )
962 ( <= last_changes_body_kid_0_width 100.0 )
963 ( >= last_changes_body_kid_0_width 100.0 )
964 ( <= last_changes_body_kid_0_hight 30.0 )
965 ( >= last_changes_body_kid_0_hight 30.0 )
966 ( <= last_changes_body_kid_1_width 300.0 )
967 ( >= last_changes_body_kid_1_width 300.0 )
968 ( <= last_changes_body_kid_1_hight 50.0 )
969 ( >= last_changes_body_kid_1_hight 50.0 )
970 ( <= last_changes_body_kid_2_width 100.0 )
971 ( >= last_changes_body_kid_2_width 100.0 )
972 ( <= last_changes_body_kid_2_hight 30.0 )
973 ( >= last_changes_body_kid_2_hight 30.0 )
974 ( <= last_changes_body_kid_3_width 300.0 )
975 ( >= last_changes_body_kid_3_width 300.0 )
976 ( <= last_changes_body_kid_3_hight 50.0 )
977 ( >= last_changes_body_kid_3_hight 50.0 )
978 ( <= last_changes_body_kid_4_width 100.0 )
979 ( >= last_changes_body_kid_4_width 100.0 )
980 ( <= last_changes_body_kid_4_hight 30.0 )
981 ( >= last_changes_body_kid_4_hight 30.0 )
982 ( <= last_changes_body_kid_5_width 300.0 )
983 ( >= last_changes_body_kid_5_width 300.0 )
984 ( <= last_changes_body_kid_5_hight 50.0 )
985 ( >= last_changes_body_kid_5_hight 50.0 )
986 ( <= last_changes_body_kid_6_width 100.0 )
987 ( >= last_changes_body_kid_6_width 100.0 )
988 ( <= last_changes_body_kid_6_hight 30.0 )
989 ( >= last_changes_body_kid_6_hight 30.0 )
990 ( <= last_changes_body_kid_7_width 300.0 )
991 ( >= last_changes_body_kid_7_width 300.0 )
992 ( <= last_changes_body_kid_7_hight 50.0 )
993 ( >= last_changes_body_kid_7_hight 50.0 )
994 ( <= last_changes_body_kid_8_width 100.0 )
995 ( >= last_changes_body_kid_8_width 100.0 )
996 ( <= last_changes_body_kid_8_hight 30.0 )
997 ( >= last_changes_body_kid_8_hight 30.0 )
998 ( >= explore_x 0.0 )
999 ( >= explore_y 0.0 )
1000 ( >= falcosecurity_x 0.0 )
1001 ( >= falcosecurity_y 0.0 )
1002 ( >= falcosecurity_width 0.0 )
1003 ( >= rustls_x 0.0 )
1004 ( >= rustls_y 0.0 )
1005 ( >= rustls_width 0.0 )
1006 ( >= contributions_x 0.0 )
1007 ( >= contributions_y 0.0 )
1008 ( >= contributions_width 0.0 )
1009 ( >= explore_more_x 0.0 )
1010 ( >= explore_more_y 0.0 )
1011 explore_repo_feasible
1012 ( <= ( + falcosecurity_y ( * -1.0 explore_y ) ) 60.0 )
1013 ( >= ( + falcosecurity_y ( * -1.0 explore_y ) ) 60.0 )
1014 ( <= ( + rustls_y ( * -1.0 falcosecurity_y ) ) 110.0 )
1015 ( >= ( + rustls_y ( * -1.0 falcosecurity_y ) ) 110.0 )
1016 ( <= ( + contributions_y ( * -1.0 rustls_y ) ) 110.0 )
1017 ( >= ( + contributions_y ( * -1.0 rustls_y ) ) 110.0 )
1018 ( <= ( + explore_more_y ( * -1.0 contributions_y ) ) 110.0 )
1019 ( >= ( + explore_more_y ( * -1.0 contributions_y ) ) 110.0 )
1020 ( <= ( + explore_repo_x ( * -1.0 explore_x ) ) -20.0 )
1021 ( >= ( + explore_repo_x explore_repo_width ( * -1.0 explore_x ) ) 120.0 )
1022 ( >= ( + explore_y ( * -1.0 explore_repo_y ) ) 20.0 )
1023 ( <= ( + explore_y ( * -1.0 explore_repo_hight ) ( * -1.0 explore_repo_y ) ) -70.0 )
1024 ( <= ( + explore_repo_x ( * -1.0 falcosecurity_x ) ) -20.0 )
1025 ( >= ( + explore_repo_x explore_repo_width ( * -1.0 falcosecurity_x ) ( * -1.0 falcosecurity_width ) ) 20.0 )
1026 ( >= ( + falcosecurity_y ( * -1.0 explore_repo_y ) ) 20.0 )
1027 ( <= ( + falcosecurity_y ( * -1.0 explore_repo_hight ) ( * -1.0 explore_repo_y ) ) -120.0 )
1028 ( <= ( + explore_repo_x ( * -1.0 rustls_x ) ) -20.0 )
1029 ( >= ( + explore_repo_x explore_repo_width ( * -1.0 rustls_x ) ( * -1.0 rustls_width ) ) 20.0 )
1030 ( >= ( + rustls_y ( * -1.0 explore_repo_y ) ) 20.0 )
1031 ( <= ( + rustls_y ( * -1.0 explore_repo_hight ) ( * -1.0 explore_repo_y ) ) -120.0 )
1032 ( >= ( + contributions_x ( * -1.0 explore_repo_x ) ) 20.0 )
1033 ( <= ( + contributions_x ( * -1.0 explore_repo_x ) contributions_width ( * -1.0 explore_repo_width ) ) -20.0 )
1034 ( >= ( + contributions_y ( * -1.0 explore_repo_y ) ) 20.0 )
1035 ( <= ( + contributions_y ( * -1.0 explore_repo_hight ) ( * -1.0 explore_repo_y ) ) -120.0 )
1036 ( <= ( + explore_repo_x ( * -1.0 explore_more_x ) ) -20.0 )
1037 ( >= ( + explore_repo_x explore_repo_width ( * -1.0 explore_more_x ) ) 120.0 )
1038 ( >= ( + explore_more_y ( * -1.0 explore_repo_y ) ) 20.0 )
1039 ( <= ( + explore_more_y ( * -1.0 explore_repo_hight ) ( * -1.0 explore_repo_y ) ) -70.0 )
1040 ( >= ( + falcosecurity_y ( * -1.0 explore_y ) ) 50.0 )
1041 ( >= ( + rustls_y ( * -1.0 falcosecurity_y ) ) 100.0 )
1042 ( >= ( + contributions_y ( * -1.0 rustls_y ) ) 100.0 )
1043 ( >= ( + explore_more_y ( * -1.0 contributions_y ) ) 100.0 )
1044 ( >= ( + explore_repo_x ( * -1.0 explore_x ) ) -20.0 )
1045 ( >= ( + explore_repo_x ( * -1.0 falcosecurity_x ) ) -20.0 )
1046 ( >= ( + explore_repo_x ( * -1.0 rustls_x ) ) -20.0 )
1047 ( <= ( + contributions_x ( * -1.0 explore_repo_x ) ) 20.0 )
1048 ( >= ( + explore_repo_x ( * -1.0 explore_more_x ) ) -20.0 )
1049 ( <= explore_width 100.0 )
1050 ( >= explore_width 100.0 )
1051 ( <= explore_hight 50.0 )
1052 ( >= explore_hight 50.0 )
1053 ( <= falcosecurity_hight 100.0 )
1054 ( >= falcosecurity_hight 100.0 )
1055 ( <= ( + explore_repo_x explore_repo_width ( * -1.0 falcosecurity_x ) ( * -1.0 falcosecurity_width ) ) 20.0 )
1056 ( <= rustls_hight 100.0 )
1057 ( >= rustls_hight 100.0 )
1058 ( <= ( + explore_repo_x explore_repo_width ( * -1.0 rustls_x ) ( * -1.0 rustls_width ) ) 20.0 )
1059 ( <= contributions_hight 100.0 )
1060 ( >= contributions_hight 100.0 )
1061 ( >= ( + contributions_x ( * -1.0 explore_repo_x ) contributions_width ( * -1.0 explore_repo_width ) ) -20.0 )
1062 ( <= explore_more_width 100.0 )
1063 ( >= explore_more_width 100.0 )
1064 ( <= explore_more_hight 50.0 )
1065 ( >= explore_more_hight 50.0 )
1066 ( >= ( + left_homes_x ( * -1.0 right_1_collom_x ) ) 0.0 )
1067 ( <= ( + left_homes_x left_homes_width ( * -1.0 right_1_collom_x ) ( * -1.0 right_1_collom_width ) ) 0.0 )
1068 ( >= ( + left_homes_y ( * -1.0 right_1_collom_y ) ) 0.0 )
1069 ( <= ( + left_homes_y left_homes_hight ( * -1.0 right_1_collom_y ) ( * -1.0 right_1_collom_hight ) ) 0.0 )
1070 ( <= home_collom_width 700.0 )
1071 ( <= right_1_collom_width 700.0 )
1072 ( >= right_1_collom_width 700.0 )
1073 ( <= ( + right_1_collom_width ( * -1.0 home_collom_width ) ) -20.0 )
1074 ( >= ( + right_1_collom_width ( * -1.0 home_collom_width ) ) -20.0 )
1075 ( <= ( + left_homes_x ( * -1.0 right_1_collom_x ) ) 0.0 )
1076 ( >= ( + left_homes_x left_homes_width ( * -1.0 right_1_collom_x ) ( * -1.0 right_1_collom_width ) ) 0.0 )
1077 ( <= ( + left_homes_y ( * -1.0 right_1_collom_y ) ) 0.0 )
1078 ( >= your_teams_x 0.0 )
1079 ( >= your_teams_y 0.0 )
1080 ( >= your_teams_width 0.0 )
1081 ( >= your_teams_hight 0.0 )
1082 ( <= ( + main_1_collom_x ( * -1.0 side_bar_x ) ) -20.0 )
1083 ( >= ( + main_1_collom_width main_1_collom_x ( * -1.0 side_bar_x ) ( * -1.0 side_bar_width ) ) 20.0 )
1084 ( >= ( + side_bar_y ( * -1.0 main_1_collom_y ) ) 20.0 )
1085 ( <= ( + side_bar_y side_bar_hight ( * -1.0 main_1_collom_y ) ( * -1.0 main_1_collom_hight ) ) -20.0 )
1086 ( >= ( + your_teams_x ( * -1.0 main_1_collom_x ) ) 20.0 )
1087 ( <= ( + your_teams_width your_teams_x ( * -1.0 main_1_collom_width ) ( * -1.0 main_1_collom_x ) ) -20.0 )
1088 ( >= ( + your_teams_y ( * -1.0 main_1_collom_y ) ) 20.0 )
1089 ( <= ( + your_teams_y your_teams_hight ( * -1.0 main_1_collom_y ) ( * -1.0 main_1_collom_hight ) ) -20.0 )
1090 ( >= ( + left_homes_x ( * -1.0 main_1_collom_x ) ) 20.0 )
1091 ( >= ( + main_1_collom_width ( * -1.0 left_homes_x ) ( * -1.0 left_homes_width ) main_1_collom_x ) 20.0 )
1092 ( >= ( + left_homes_y ( * -1.0 main_1_collom_y ) ) 20.0 )
1093 ( <= ( + left_homes_y ( * -1.0 main_1_collom_y ) ( * -1.0 main_1_collom_hight ) left_homes_hight ) -20.0 )
1094 ( >= ( + your_teams_y ( * -1.0 side_bar_y ) ( * -1.0 side_bar_hight ) ) 0.0 )
1095 ( <= ( + your_teams_y your_teams_hight ( * -1.0 left_homes_y ) ) 0.0 )
1096 ( <= ( + your_teams_y ( * -1.0 side_bar_y ) ( * -1.0 side_bar_hight ) ) 20.0 )
1097 ( >= ( + your_teams_y ( * -1.0 side_bar_y ) ( * -1.0 side_bar_hight ) ) 20.0 )
1098 ( <= ( + your_teams_y your_teams_hight ( * -1.0 left_homes_y ) ) -20.0 )
1099 ( >= ( + your_teams_y your_teams_hight ( * -1.0 left_homes_y ) ) -20.0 )
1100 ( >= ( + main_1_collom_x ( * -1.0 side_bar_x ) ) -20.0 )
1101 ( <= ( + main_1_collom_width main_1_collom_x ( * -1.0 side_bar_x ) ( * -1.0 side_bar_width ) ) 20.0 )
1102 ( <= ( + your_teams_x ( * -1.0 main_1_collom_x ) ) 20.0 )
1103 ( >= ( + your_teams_width your_teams_x ( * -1.0 main_1_collom_width ) ( * -1.0 main_1_collom_x ) ) -20.0 )
1104 ( <= ( + left_homes_x ( * -1.0 main_1_collom_x ) ) 20.0 )
1105 ( <= ( + main_1_collom_width ( * -1.0 left_homes_x ) ( * -1.0 left_homes_width ) main_1_collom_x ) 20.0 )
1106 ( >= team_name_x 0.0 )
1107 ( >= team_name_y 0.0 )
1108 ( >= teams_list_x 0.0 )
1109 ( >= teams_list_y 0.0 )
1110 ( >= teams_list_width 0.0 )
1111 ( >= teams_list_hight 0.0 )
1112 your_teams_feasible
1113 ( <= ( + team_name_y ( * -1.0 teams_list_y ) ) -70.0 )
1114 ( >= ( + team_name_y ( * -1.0 teams_list_y ) ) -70.0 )
1115 ( <= ( + your_teams_x ( * -1.0 team_name_x ) ) -20.0 )
1116 ( >= ( + your_teams_width your_teams_x ( * -1.0 team_name_x ) ) 120.0 )
1117 ( >= ( + team_name_y ( * -1.0 your_teams_y ) ) 20.0 )
1118 ( <= ( + team_name_y ( * -1.0 your_teams_y ) ( * -1.0 your_teams_hight ) ) -70.0 )
1119 ( >= ( + teams_list_x ( * -1.0 your_teams_x ) ) 20.0 )
1120 ( >= ( + your_teams_width ( * -1.0 teams_list_x ) your_teams_x ( * -1.0 teams_list_width ) ) 20.0 )
1121 ( >= ( + teams_list_y ( * -1.0 your_teams_y ) ) 20.0 )
1122 ( <= ( + teams_list_hight teams_list_y ( * -1.0 your_teams_y ) ( * -1.0 your_teams_hight ) ) -20.0 )
1123 ( <= ( + team_name_y ( * -1.0 teams_list_y ) ) -50.0 )
1124 ( >= ( + your_teams_x ( * -1.0 team_name_x ) ) -20.0 )
1125 ( <= ( + teams_list_x ( * -1.0 your_teams_x ) ) 20.0 )
1126 ( <= team_name_width 100.0 )
1127 ( >= team_name_width 100.0 )
1128 ( <= team_name_hight 50.0 )
1129 ( >= team_name_hight 50.0 )
1130 ( <= ( + your_teams_width ( * -1.0 teams_list_x ) your_teams_x ( * -1.0 teams_list_width ) ) 20.0 )
1131 ( <= teams_list_hight 100.0 )
1132 ( >= teams_list_hight 100.0 )
1133 back_ground_feasible
1134 title_feasible
1135 main_holder_feasible
1136 less_icon_feasible
1137 github_icon_feasible
1138 dashbord_feasible
1139 search_holder_feasible
1140 mails_holder_feasible
1141 search_bar_1_kid_0_feasible
1142 search_bar_1_kid_1_feasible
1143 add_feasible
1144 point_feasible
1145 pull_feasible
1146 mail_feasible
1147 person_feasible
1148 user_name_feasible
1149 top_repo_feasible
1150 find_repo_feasible
1151 show_more_feasible
1152 repos_kid_0_feasible
1153 repos_kid_1_feasible
1154 repos_kid_2_feasible
1155 repos_kid_3_feasible
1156 repos_kid_4_feasible
1157 repos_kid_5_feasible
1158 repos_kid_6_feasible
1159 home_icon_feasible
1160 send_feedback_feasible
1161 filter_feasible
1162 z3_icon_feasible
1163 z3_version_feasible
1164 changes_feasible
1165 z3_smile_feasible
1166 cvc_icon_feasible
1167 cvc_version_feasible
1168 cvc_changes_feasible
1169 cvc_smile_feasible
1170 recomend_for_you_feasible
1171 boolect_feasible
1172 stars_feasible
1173 rec_word_feasible
1174 rec_left_icon_feasible
1175 rec_right_icon_feasible
1176 last_changes_title_feasible
1177 last_changes_body_kid_0_feasible
1178 last_changes_body_kid_1_feasible
1179 last_changes_body_kid_2_feasible
1180 last_changes_body_kid_3_feasible
1181 last_changes_body_kid_4_feasible
1182 last_changes_body_kid_5_feasible
1183 last_changes_body_kid_6_feasible
1184 last_changes_body_kid_7_feasible
1185 last_changes_body_kid_8_feasible
1186 explore_feasible
1187 falcosecurity_feasible
1188 rustls_feasible
1189 contributions_feasible
1190 explore_more_feasible
1191 team_name_feasible
1192 teams_list_feasible
0
1376
( 1 )
( 2 )
( 3 )
( 4 )
( 5 )
( 6 )
( 7 )
( 8 )
( 9 )
( 10 )
( 11 )
( 12 )
( 13 )
( 14 )
( 15 )
( 16 )
( 17 )
( 18 )
( 19 )
( 20 )
( 21 )
( 22 )
( 23 )
( 24 )
( 25 )
( 26 )
( 27 )
( 28 )
( 16 )
( 19 )
( 29 )
( 30 )
( 31 )
( 32 )
( 33 )
( 34 )
( 35 )
( 36 )
( 37 )
( 38 )
( 39 )
( 40 )
( 41 )
( 42 )
( 43 )
( 44 )
( 45 )
( 46 )
( 47 )
( 48 )
( 49 )
( 50 )
( 51 )
( 52 )
( 53 )
( 54 )
( 55 )
( 56 )
( 57 )
( 58 )
( 59 )
( 60 )
( 61 )
( 62 )
( 63 )
( 64 )
( 65 )
( 66 )
( 67 )
( 68 )
( 69 )
( 70 )
( 71 )
( 72 )
( 73 )
( 74 )
( 75 )
( 76 )
( 77 )
( 78 )
( 79 )
( 80 )
( 81 )
( 82 )
( 83 )
( 84 )
( 85 )
( 86 )
( 87 )
( 88 )
( 89 )
( 90 )
( 91 )
( 92 )
( 93 )
( 94 )
( 95 )
( 96 )
( 97 )
( 98 )
( 99 )
( 100 )
( 101 )
( 102 )
( 103 )
( 104 )
( 105 )
( -106 107 )
( -106 108 )
( -106 109 )
( -106 110 )
( -106 111 )
( -106 112 )
( -106 113 )
( -106 114 )
( -115 116 )
( -115 117 )
( -115 118 )
( -115 119 )
( -115 120 )
( -115 121 )
( -115 122 )
( -115 123 )
( 106 115 )
( -106 -115 )
( 124 )
( 125 )
( 126 )
( 127 )
( 128 )
( 129 )
( 130 )
( 131 )
( 132 )
( 133 )
( 134 )
( 135 )
( 136 )
( -106 137 )
( -106 138 )
( -106 139 )
( -106 140 )
( -106 141 )
( -106 142 )
( -106 143 )
( -106 144 )
( -106 145 )
( -106 146 )
( -106 147 )
( -106 148 )
( -106 149 )
( -106 150 )
( -106 151 )
( -106 152 )
( 153 )
( 154 )
( 155 )
( 156 )
( 157 )
( 158 )
( 159 )
( 160 )
( -161 162 )
( -161 163 )
( -161 164 )
( -161 165 )
( -161 166 )
( -161 167 )
( -161 168 )
( -161 169 )
( -170 171 )
( -170 172 )
( -170 173 )
( -170 174 )
( -170 175 )
( -170 176 )
( -170 177 )
( -170 178 )
( 161 170 )
( -161 -170 )
( 179 )
( 180 )
( 181 )
( 182 )
( 183 )
( 184 )
( 185 )
( 186 )
( 187 )
( 188 )
( 189 )
( 190 )
( 191 )
( 192 )
( 193 )
( 194 )
( 195 )
( -161 196 )
( -161 197 )
( -161 198 )
( -161 199 )
( -161 200 )
( -161 201 )
( -161 202 )
( -161 203 )
( -161 204 )
( -161 205 )
( -161 206 )
( -161 207 )
( -161 208 )
( -161 209 )
( -161 210 )
( -161 211 )
( -161 212 )
( -161 213 )
( -161 214 )
( -161 215 )
( -161 216 )
( -161 217 )
( -161 218 )
( -161 219 )
( -161 220 )
( -161 196 )
( -161 213 )
( -161 221 )
( -161 198 )
( -161 222 )
( -161 202 )
( -161 223 )
( -161 206 )
( -161 224 )
( -161 225 )
( -161 210 )
( -161 226 )
( -161 214 )
( -161 227 )
( -161 199 )
( -161 228 )
( -161 203 )
( -161 229 )
( -161 207 )
( -161 211 )
( -161 230 )
( -161 215 )
( -161 231 )
( -161 232 )
( -161 233 )
( -161 234 )
( -161 235 )
( -161 236 )
( -161 237 )
( -161 238 )
( -161 239 )
( 240 )
( 241 )
( 242 )
( 243 )
( 244 )
( 245 )
( 246 )
( 247 )
( 248 )
( 249 )
( -170 250 )
( -170 251 )
( -170 252 )
( -170 253 )
( -170 254 )
( -170 255 )
( -170 256 )
( -170 257 )
( -170 258 )
( -170 259 )
( -170 260 )
( -170 261 )
( -170 238 )
( -170 239 )
( -170 251 )
( -170 262 )
( -170 254 )
( -170 259 )
( -170 263 )
( -170 252 )
( -170 256 )
( -170 261 )
( -170 219 )
( 264 )
( 265 )
( 266 )
( 267 )
( 268 )
( 269 )
( 270 )
( 271 )
( -272 273 )
( -272 274 )
( -272 275 )
( -272 276 )
( -272 277 )
( -272 278 )
( -272 279 )
( -272 280 )
( -281 282 )
( -281 283 )
( -281 284 )
( -281 285 )
( -281 286 )
( -281 287 )
( -281 288 )
( -281 289 )
( 272 281 )
( -272 -281 )
( 290 )
( 291 )
( 292 )
( 293 )
( 294 )
( 295 )
( 296 )
( 297 )
( -272 298 )
( -272 299 )
( -272 300 )
( -272 301 )
( -272 302 )
( -272 303 )
( -272 304 )
( -272 305 )
( -272 306 )
( -272 307 )
( -272 298 )
( -272 303 )
( -272 308 )
( -272 309 )
( -272 300 )
( -272 310 )
( -272 304 )
( -272 301 )
( -272 311 )
( -272 305 )
( -272 312 )
( -272 306 )
( -272 313 )
( 314 )
( 315 )
( 316 )
( 317 )
( 318 )
( 319 )
( 320 )
( 321 )
( 322 )
( 323 )
( 324 )
( 325 )
( 326 )
( 327 )
( 328 )
( -329 330 )
( -329 331 )
( -329 332 )
( -329 333 )
( -329 334 )
( -329 335 )
( -329 336 )
( -329 337 )
( -329 338 )
( -329 339 )
( -329 340 )
( -329 341 )
( -329 342 )
( -329 343 )
( -329 344 )
( -329 345 )
( -329 346 )
( -329 347 )
( -329 348 )
( -329 349 )
( -329 350 )
( -329 351 )
( -329 352 )
( -329 353 )
( -329 354 )
( -329 355 )
( -329 356 )
( -329 357 )
( -329 358 )
( -329 359 )
( -329 360 )
( -329 361 )
( -272 362 )
( -272 363 )
( -329 338 )
( -329 364 )
( -329 342 )
( -329 365 )
( -329 346 )
( -329 366 )
( -329 350 )
( -329 367 )
( -329 354 )
( -329 368 )
( 369 )
( 370 )
( -329 371 )
( -329 372 )
( -329 340 )
( -329 373 )
( 374 )
( 375 )
( -329 376 )
( -329 343 )
( 377 )
( 378 )
( -329 379 )
( -329 347 )
( 380 )
( 381 )
( -329 382 )
( -329 351 )
( 383 )
( 384 )
( 385 )
( 386 )
( 387 )
( 388 )
( 389 )
( 390 )
( 391 )
( 392 )
( 393 )
( 394 )
( 395 )
( 396 )
( 397 )
( 398 )
( 399 )
( 400 )
( 401 )
( 402 )
( 403 )
( 404 )
( 405 )
( 406 )
( 407 )
( 408 )
( 409 )
( 410 )
( -411 412 )
( -411 413 )
( -411 414 )
( -411 415 )
( -411 416 )
( -411 417 )
( -411 418 )
( -411 419 )
( -411 420 )
( -411 421 )
( -411 422 )
( -411 423 )
( -411 424 )
( -411 425 )
( -411 426 )
( -411 427 )
( -411 428 )
( -411 429 )
( -411 430 )
( -411 431 )
( -411 432 )
( -411 433 )
( -411 434 )
( -411 435 )
( -411 436 )
( -411 437 )
( -411 438 )
( -411 439 )
( -411 440 )
( -411 441 )
( -411 442 )
( -411 443 )
( -411 444 )
( -411 445 )
( -411 446 )
( -411 447 )
( -411 448 )
( -411 449 )
( -411 450 )
( -411 451 )
( -411 452 )
( -411 453 )
( -411 454 )
( -411 455 )
( -411 456 )
( -411 457 )
( -411 458 )
( -411 459 )
( -411 460 )
( -411 461 )
( -411 462 )
( -411 463 )
( -411 464 )
( -411 465 )
( -411 466 )
( -411 467 )
( 468 )
( 469 )
( -329 470 )
( -329 471 )
( 472 )
( 473 )
( 474 )
( 475 )
( -476 477 )
( -476 478 )
( -476 479 )
( -476 480 )
( 481 )
( 482 )
( 483 )
( 484 )
( 485 )
( 486 )
( 487 )
( 488 )
( -489 490 )
( -489 491 )
( -489 492 )
( -489 493 )
( -489 494 )
( -489 495 )
( -489 496 )
( -489 497 )
( -498 499 )
( -498 500 )
( -498 501 )
( -498 502 )
( -498 503 )
( -498 504 )
( -498 505 )
( -498 506 )
( 489 498 -507 )
( -489 -498 -507 )
( 508 )
( 509 )
( -476 510 )
( -476 511 )
( 512 )
( 513 )
( 514 )
( 515 )
( 516 )
( 517 )
( 518 )
( -489 519 )
( -489 520 )
( -489 521 )
( -489 522 )
( -489 523 )
( -489 524 )
( -489 525 )
( -489 526 )
( -489 527 )
( 528 529 )
( 528 530 )
( -528 531 )
( -528 532 )
( 533 )
( 534 )
( 535 )
( 536 )
( 537 )
( 538 )
( 539 )
( 540 )
( 541 )
( 542 )
( 543 )
( 544 )
( 545 )
( 546 )
( 547 )
( -548 549 )
( -548 550 )
( -548 551 )
( -548 552 )
( -548 553 )
( -548 554 )
( -548 555 )
( -548 556 )
( -548 557 )
( -548 558 )
( -548 559 )
( -548 560 )
( -548 561 )
( -548 562 )
( -548 563 )
( -548 564 )
( -548 565 )
( -548 566 )
( -548 567 )
( -548 568 )
( -548 569 )
( -548 570 )
( -548 571 )
( -548 572 )
( -548 573 )
( -548 574 )
( -548 549 )
( -548 558 )
( -548 565 )
( -548 575 )
( -548 551 )
( -548 560 )
( -548 576 )
( -548 577 )
( -548 553 )
( -548 562 )
( -548 578 )
( -548 579 )
( -548 555 )
( -548 564 )
( -548 580 )
( -548 568 )
( -548 581 )
( -548 582 )
( -548 583 )
( -489 584 )
( -489 521 )
( -548 -585 )
( 586 )
( 587 )
( 588 )
( 589 )
( 590 )
( 591 )
( 592 )
( 593 )
( 594 )
( 595 )
( 596 )
( 597 )
( 598 )
( 599 )
( -600 601 )
( -600 602 )
( -600 603 )
( -600 604 )
( -600 605 )
( -600 606 )
( -600 607 )
( -600 608 )
( -600 609 )
( -600 610 )
( -600 611 )
( -600 612 )
( -600 613 )
( -600 614 )
( -600 615 )
( -600 616 )
( -600 602 )
( -600 617 )
( -600 605 )
( -600 612 )
( -600 618 )
( -600 619 )
( -600 607 )
( -600 614 )
( -600 620 )
( -600 603 )
( -600 609 )
( -600 616 )
( -600 621 )
( -600 622 )
( -600 623 )
( -600 624 )
( -600 625 )
( -600 626 )
( -600 627 )
( -600 628 )
( -600 629 )
( -600 630 )
( 631 )
( 632 )
( 633 )
( 634 )
( 635 )
( 636 )
( 637 )
( 638 )
( 639 )
( -640 641 )
( -640 642 )
( -640 643 )
( -640 644 )
( -640 645 )
( -640 646 )
( -640 647 )
( -640 648 )
( -640 649 )
( -640 650 )
( -640 651 )
( -640 652 )
( -640 653 )
( -640 654 )
( -640 655 )
( -640 656 )
( -640 657 )
( -640 658 )
( -640 659 )
( -640 660 )
( -640 661 )
( -640 662 )
( -640 663 )
( -640 664 )
( -640 665 )
( -640 647 )
( -640 666 )
( -640 651 )
( -640 667 )
( -640 655 )
( -640 668 )
( -640 659 )
( -640 669 )
( 670 )
( 671 )
( 672 )
( 673 )
( 674 )
( 675 )
( 676 )
( 677 )
( 678 )
( 679 )
( -640 680 )
( -640 656 )
( -640 681 )
( -640 662 )
( 682 )
( 683 )
( 684 )
( 685 )
( -640 649 )
( -640 686 )
( 687 )
( 688 )
( 689 )
( 690 )
( 691 )
( 692 )
( 693 )
( 694 )
( 695 )
( -696 697 )
( -696 698 )
( -696 699 )
( -696 700 )
( -696 701 )
( -696 702 )
( -696 703 )
( -696 704 )
( -696 705 )
( -696 706 )
( -696 707 )
( -696 708 )
( -696 709 )
( -696 710 )
( -696 711 )
( -696 712 )
( -696 713 )
( -696 714 )
( -696 715 )
( -696 716 )
( -696 717 )
( -696 718 )
( -696 719 )
( -696 720 )
( -696 721 )
( -696 703 )
( -696 722 )
( -696 707 )
( -696 723 )
( -696 711 )
( -696 724 )
( -696 715 )
( -696 725 )
( 726 )
( 727 )
( 728 )
( 729 )
( 730 )
( 731 )
( 732 )
( 733 )
( 734 )
( 735 )
( -696 712 )
( -696 736 )
( -696 737 )
( -696 718 )
( 738 )
( 739 )
( 740 )
( 741 )
( -696 705 )
( -696 742 )
( 743 )
( 744 )
( -745 746 )
( -745 747 )
( -745 748 )
( -745 749 )
( 750 )
( 751 )
( 752 )
( 753 )
( 754 )
( 755 )
( 756 )
( 757 )
( 758 )
( 759 )
( -745 760 )
( -745 761 )
( -745 762 )
( -745 763 )
( 764 )
( 765 )
( 766 )
( -745 767 )
( -745 768 )
( -745 769 )
( -745 770 )
( -745 771 )
( -745 772 )
( 773 )
( 774 )
( 775 )
( 776 )
( 777 )
( -745 778 )
( -745 779 )
( -745 780 )
( -745 781 )
( 782 )
( 783 )
( -745 784 )
( -745 785 )
( 786 )
( 787 )
( -745 788 )
( -745 789 )
( -745 790 )
( -745 791 )
( 792 )
( 793 )
( 794 )
( 795 )
( 796 )
( 797 )
( -745 798 )
( -745 799 )
( -745 800 )
( -745 801 )
( 802 )
( 803 )
( 804 )
( 805 )
( -745 806 )
( -745 807 )
( 808 )
( 809 )
( 810 )
( 811 )
( 812 )
( 813 )
( 814 )
( 815 )
( -816 817 )
( -816 818 )
( -816 819 )
( -816 820 )
( -816 821 )
( -816 822 )
( -816 823 )
( -816 824 )
( -816 825 )
( -816 826 )
( -816 827 )
( -816 828 )
( -816 818 )
( -816 821 )
( -816 826 )
( -816 829 )
( -816 820 )
( -816 823 )
( -816 830 )
( -816 827 )
( -816 831 )
( -816 832 )
( -816 833 )
( 834 )
( 835 )
( 836 )
( 837 )
( 838 )
( 839 )
( 840 )
( 841 )
( 842 )
( 843 )
( 844 )
( 845 )
( 846 )
( 847 )
( -848 849 )
( -848 850 )
( -848 851 )
( -848 852 )
( -848 853 )
( -848 854 )
( -848 855 )
( -848 856 )
( -848 857 )
( -848 858 )
( -848 859 )
( -848 860 )
( -848 861 )
( -848 862 )
( -848 863 )
( -848 864 )
( -848 865 )
( -848 866 )
( -848 867 )
( -848 868 )
( -848 869 )
( -848 870 )
( -848 871 )
( -848 872 )
( -848 873 )
( 874 )
( 875 )
( 876 )
( 877 )
( 878 )
( 879 )
( 880 )
( 881 )
( 882 )
( 883 )
( 884 )
( 885 )
( 886 )
( 887 )
( 888 )
( 889 )
( 890 )
( 891 )
( -892 893 )
( -892 894 )
( -892 895 )
( -892 896 )
( -892 897 )
( -892 898 )
( -892 899 )
( -892 900 )
( -892 901 )
( -892 902 )
( -892 903 )
( -892 904 )
( -892 905 )
( -892 906 )
( -892 907 )
( -892 908 )
( -892 909 )
( -892 910 )
( -892 911 )
( -892 912 )
( -892 913 )
( -892 914 )
( -892 915 )
( -892 916 )
( -892 917 )
( -892 918 )
( -892 919 )
( -892 920 )
( -892 921 )
( -892 922 )
( -892 923 )
( -892 924 )
( -892 925 )
( -892 926 )
( -892 927 )
( -892 928 )
( -892 929 )
( -892 930 )
( -892 931 )
( -892 932 )
( -892 933 )
( -892 934 )
( -892 935 )
( -892 936 )
( -892 893 )
( -892 937 )
( -892 897 )
( -892 938 )
( -892 901 )
( -892 939 )
( -892 905 )
( -892 940 )
( -892 909 )
( -892 941 )
( -892 913 )
( -892 942 )
( -892 917 )
( -892 943 )
( -892 921 )
( -892 944 )
( -892 925 )
( -892 945 )
( -892 946 )
( -892 947 )
( -892 948 )
( -892 949 )
( -892 950 )
( -892 951 )
( -892 952 )
( -892 953 )
( -892 954 )
( -892 955 )
( -892 956 )
( -892 957 )
( -892 958 )
( -892 959 )
( -892 960 )
( -892 961 )
( 962 )
( 963 )
( 964 )
( 965 )
( 966 )
( 967 )
( 968 )
( 969 )
( 970 )
( 971 )
( 972 )
( 973 )
( 974 )
( 975 )
( 976 )
( 977 )
( 978 )
( 979 )
( 980 )
( 981 )
( 982 )
( 983 )
( 984 )
( 985 )
( 986 )
( 987 )
( 988 )
( 989 )
( 990 )
( 991 )
( 992 )
( 993 )
( 994 )
( 995 )
( 996 )
( 997 )
( 998 )
( 999 )
( 1000 )
( 1001 )
( 1002 )
( 1003 )
( 1004 )
( 1005 )
( 1006 )
( 1007 )
( 1008 )
( 1009 )
( 1010 )
( -1011 1012 )
( -1011 1013 )
( -1011 1014 )
( -1011 1015 )
( -1011 1016 )
( -1011 1017 )
( -1011 1018 )
( -1011 1019 )
( -1011 1020 )
( -1011 1021 )
( -1011 1022 )
( -1011 1023 )
( -1011 1024 )
( -1011 1025 )
( -1011 1026 )
( -1011 1027 )
( -1011 1028 )
( -1011 1029 )
( -1011 1030 )
( -1011 1031 )
( -1011 1032 )
( -1011 1033 )
( -1011 1034 )
( -1011 1035 )
( -1011 1036 )
( -1011 1037 )
( -1011 1038 )
( -1011 1039 )
( -1011 1040 )
( -1011 1041 )
( -1011 1042 )
( -1011 1043 )
( -1011 1020 )
( -1011 1044 )
( -1011 1024 )
( -1011 1045 )
( -1011 1028 )
( -1011 1046 )
( -1011 1047 )
( -1011 1032 )
( -1011 1036 )
( -1011 1048 )
( 1049 )
( 1050 )
( 1051 )
( 1052 )
( 1053 )
( 1054 )
( -1011 1055 )
( -1011 1025 )
( 1056 )
( 1057 )
( -1011 1058 )
( -1011 1029 )
( 1059 )
( 1060 )
( -1011 1033 )
( -1011 1061 )
( 1062 )
( 1063 )
( 1064 )
( 1065 )
( -498 1066 )
( -498 1067 )
( -498 1068 )
( -498 1069 )
( 1070 1071 )
( 1070 1072 )
( -1070 1073 )
( -1070 1074 )
( -498 1075 )
( -498 1066 )
( -498 1067 )
( -498 1076 )
( -498 1077 )
( -498 1068 )
( 1078 )
( 1079 )
( 1080 )
( 1081 )
( -281 1082 )
( -281 1083 )
( -281 1084 )
( -281 1085 )
( -281 1086 )
( -281 1087 )
( -281 1088 )
( -281 1089 )
( -281 1090 )
( -281 1091 )
( -281 1092 )
( -281 1093 )
( -281 1094 )
( -281 1095 )
( -281 1096 )
( -281 1097 )
( -281 1098 )
( -281 1099 )
( -281 1082 )
( -281 1100 )
( -281 1101 )
( -281 1083 )
( -281 1102 )
( -281 1086 )
( -281 1087 )
( -281 1103 )
( -281 1104 )
( -281 1090 )
( -281 1105 )
( -281 1091 )
( 1106 )
( 1107 )
( 1108 )
( 1109 )
( 1110 )
( 1111 )
( -1112 1113 )
( -1112 1114 )
( -1112 1115 )
( -1112 1116 )
( -1112 1117 )
( -1112 1118 )
( -1112 1119 )
( -1112 1120 )
( -1112 1121 )
( -1112 1122 )
( -1112 1123 )
( -1112 1115 )
( -1112 1124 )
( -1112 1125 )
( -1112 1119 )
( 1126 )
( 1127 )
( 1128 )
( 1129 )
( -1112 1130 )
( -1112 1120 )
( -1112 1131 )
( -1112 1132 )
( 1133 )
( 1134 )
( 1135 )
( 1136 )
( 1137 )
( 1138 )
( 1139 )
( 1140 )
( 106 -1141 )
( -106 1141 )
( 106 -1142 )
( -106 1142 )
( 161 -1143 )
( -161 1143 )
( 161 -1144 )
( -161 1144 )
( 161 -1145 )
( -161 1145 )
( -161 1146 )
( -170 1146 )
( 161 170 -1146 )
( -161 -170 -1146 )
( -161 1147 )
( -170 1147 )
( 161 170 -1147 )
( -161 -170 -1147 )
( -272 329 )
( -281 329 )
( 272 281 -329 )
( -272 -281 -329 )
( 272 -476 )
( -272 476 )
( 329 -1148 )
( -329 1148 )
( 329 -1149 )
( -329 1149 )
( 329 -1150 )
( -329 1150 )
( 329 -411 )
( -329 411 )
( 329 -1151 )
( -329 1151 )
( 411 -1152 )
( -411 1152 )
( 411 -1153 )
( -411 1153 )
( 411 -1154 )
( -411 1154 )
( 411 -1155 )
( -411 1155 )
( 411 -1156 )
( -411 1156 )
( 411 -1157 )
( -411 1157 )
( 411 -1158 )
( -411 1158 )
( 476 -507 )
( -476 507 )
( -489 507 )
( -498 507 )
( -489 548 )
( -498 548 )
( -281 548 )
( 281 489 498 -548 )
( -489 -498 -548 )
( -281 -489 -548 )
( -281 -498 -548 )
( 489 -816 )
( -489 816 )
( 548 -600 )
( -548 600 )
( 548 -640 )
( -548 640 )
( 548 -696 )
( -548 696 )
( 548 -745 )
( -548 745 )
( 600 -1159 )
( -600 1159 )
( 600 -1160 )
( -600 1160 )
( 600 -1161 )
( -600 1161 )
( 640 -1162 )
( -640 1162 )
( 640 -1163 )
( -640 1163 )
( 640 -1164 )
( -640 1164 )
( 640 -1165 )
( -640 1165 )
( 696 -1166 )
( -696 1166 )
( 696 -1167 )
( -696 1167 )
( 696 -1168 )
( -696 1168 )
( 696 -1169 )
( -696 1169 )
( 745 -1170 )
( -745 1170 )
( 745 -1171 )
( -745 1171 )
( 745 -1172 )
( -745 1172 )
( 745 -1173 )
( -745 1173 )
( 745 -1174 )
( -745 1174 )
( 745 -1175 )
( -745 1175 )
( 816 -848 )
( -816 848 )
( 816 -1011 )
( -816 1011 )
( 848 -1176 )
( -848 1176 )
( 848 -892 )
( -848 892 )
( 892 -1177 )
( -892 1177 )
( 892 -1178 )
( -892 1178 )
( 892 -1179 )
( -892 1179 )
( 892 -1180 )
( -892 1180 )
( 892 -1181 )
( -892 1181 )
( 892 -1182 )
( -892 1182 )
( 892 -1183 )
( -892 1183 )
( 892 -1184 )
( -892 1184 )
( 892 -1185 )
( -892 1185 )
( 1011 -1186 )
( -1011 1186 )
( 1011 -1187 )
( -1011 1187 )
( 1011 -1188 )
( -1011 1188 )
( 1011 -1189 )
( -1011 1189 )
( 1011 -1190 )
( -1011 1190 )
( 281 -1112 )
( -281 1112 )
( 1112 -1191 )
( -1112 1191 )
( 1112 -1192 )
( -1112 1192 )
sat
